# 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:
>Hi,
>
>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:
>>
>> lemma
>> shows "not something"
>> proof
>> assume "something"
>> hence False proof cases
>> ...
>> qed
>> thus False by simp
>> qed
>
>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
>used...)
>
>Such features give great insight into the system and give the users more
>confidence in using it.
>
>Greetings,
>Joachim
>
>--
>Dipl.-Math. Dipl.-Inform. Joachim Breitner
>Wissenschaftlicher Mitarbeiter
>http://pp.ipd.kit.edu/~breitner

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*