Re: [isabelle] Unfortunate Display problem
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,
Jens-Wolfhard Schicke wrote:
-----BEGIN PGP SIGNED MESSAGE-----
Hi, I discovered an unfortunate display problem, if not bug:
assumes assm: "P t"
shows "\<all>t. P t"
proof (rule allI)
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.
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.9 (GNU/Linux)
-----END PGP SIGNATURE-----
This archive was generated by a fusion of
Pipermail (Mailman edition) and