[isabelle] lemmas-command normalizes theorems



Hi,

I stumbled over the following (unexpected, undocumented) behaviour of
the lemmas command:

thm norm_hhf_eq
(* (PROP ?phi ==> (!!x. PROP ?psi x)) 
  == (!!x. PROP ?phi ==> PROP ?psi x) *)
lemmas foo = norm_hhf_eq
(* lemma foo: (!!x. PROP ?phi ==> PROP ?psi x) 
  == (!!x. PROP ?phi ==> PROP ?psi x) *)

So, obviously, there is some normalization going on. What normalization
is exactly applied? 
The isar-ref manual says:
  "Results are standardized before being stored, i.e. schematic
   variables are renamed to enforce index 0 uniformly."

but nothing about other normalizations.


Is there a way, other than raw isabelle-ML declaration, to avoid this
normalization and just give a name to a list of theorems?

--
  Peter





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