[isabelle] Unfortunate Display problem



-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Hi, I discovered an unfortunate display problem, if not bug:

lemma bug:
assumes assm: "P t"
shows "\<all>t. P t"
proof (rule allI)
  fix t
  show "P t"
  apply (insert assm)    (* Proof state:    P t ==> P t  *)
  apply assumption       (* Fails, which is A Good Thing *)

In particular the insert should either warn about doubly used variable
names or rename some other variable.

Best Regards,
  Jens
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.9 (GNU/Linux)

iEYEARECAAYFAkkzsL0ACgkQzhchXT4RR5BwzgCfZvnfxGdXvwg0i+EouzO3+RDH
foMAnjAUqOASaP28NHfA9cCRKWDZwByN
=kqgw
-----END PGP SIGNATURE-----





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