# [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.*