On 08/24/2010 09:13 PM, Andreas Schropp wrote:
On 08/24/2010 07:51 PM, Alexander Krauss wrote:
lemma fixes x shows "A x ==> B x"
apply method
and
lemma fixes x
assumes a: "A x"
shows "B x"
apply (insert a)
apply method
Safe or not, this is obviously undesirable.
BTW: if you want to be even more conservative you
take both fixes and assumes into account
(are the Frees in assumes always guaranteed to be fixed?)
when approximating safeness of equality-elimination.
Then you would have to compare e.g.
lemma shows "!! x. A x ==> B x"
apply method
and
lemma fixes x
assumes a: "A x"
shows "B x"
apply (insert a)
apply method
to observe the difference. Is that better or worse? ^^
_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
