Re: [isabelle] Isar syntax question
I agree. If I remember correctly, a crude form of that is provided by the rule_trace option.
Joachim Breitner <breitner at kit.edu> schrieb:
>Am Mittwoch, den 16.07.2014, 15:00 -0700 schrieb Vadim Zaliva:
>> I am learning Isar and have another naive question on the syntax:
>> I am trying to do something like this in Isar:
>> 1: lemma
>> 2: shows "not something"
>> 3: proof(rule ccontr)
>> 4: assume "something"
>> 5: thus False proof cases
>> 6: ...
>> 7: qed
>> 8: qed
>> and get "*** Failed to refine any pending goal" error around line 5
>> Why this does not work? Something like this works instead:
>> shows "not something"
>> assume "something"
>> hence False proof cases
>> thus False by simp
>it would be very helpful, especially for beginners, but often also for
>me, if a "proof" would tell us what rule it applied – similar to how
>"also" tells us what the current calculation is.
>(And while are are at it: "also" could also tell us what rule it
>Such features give great insight into the system and give the users more
>confidence in using it.
>Dipl.-Math. Dipl.-Inform. Joachim Breitner
This archive was generated by a fusion of
Pipermail (Mailman edition) and