| changeset 14171 | 0cab06e3bbd0 |
| parent 13688 | a0b16d42d489 |
| child 14766 | c0401da7726d |
--- a/src/HOL/Bali/Type.thy Wed Aug 27 18:22:34 2003 +0200 +++ b/src/HOL/Bali/Type.thy Thu Aug 28 01:56:40 2003 +0200 @@ -51,7 +51,7 @@ constdefs the_Class :: "ty \<Rightarrow> qtname" - "the_Class T \<equiv> \<epsilon>C. T = Class C" (** primrec not possible here **) + "the_Class T \<equiv> \<epsilon> C. T = Class C" (** primrec not possible here **) lemma the_Class_eq [simp]: "the_Class (Class C)= C" by (auto simp add: the_Class_def)