Re: [isabelle] Unfortunate Display problem



Hi Jens,

The System somehow warns you in the following sense:
Lokk at the proof state after

apply (insert assm)

Then you will notice that one t is "brown" and the other is blue. These colors have a meaning and they depend on the nature of the binding/declaration of the variables, which gives you some insight about what you are writing.

This feature saved me a lot of time on several occasions!

Hope it helps,
Amine.

Jens-Wolfhard Schicke wrote:
-----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.