Re: [isabelle] term abbreviations?



The following (not widely advertised) feature may help. You can always refer to subgoals i by "case goal<i>", which sets ?case to the actual subgoal. Here is a (bad!) example:

lemma "P & Q"
proof(rule conjI)
  case goal1
  show ?case sorry
next
  case goal2
  show ?case sorry
qed

?case stands for P/Q in subgoal 1/2.

This feature does not yield readable proofs but helps in situations like you describe.

Tobias

David Streader schrieb:
In constructing some proof that have complexe goals formaed by unfolding locale definitions
I have been  cut and pasting  the goal  in to a show statment

show "......complex gaol ...." (is  patten)

After which I only refer to the patten.
Is there a term abbreviation for current gaol or other method to avoid the cut and pasting?
david





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