changeset 26242 | d64510d3c7b7 |
parent 26168 | 3bd9ac4e0b97 |
child 26267 | ba710daf77a7 |
--- a/src/HOL/Library/Eval.thy Fri Mar 07 16:46:57 2008 +0100 +++ b/src/HOL/Library/Eval.thy Sun Mar 09 07:57:30 2008 +0100 @@ -33,7 +33,6 @@ subsubsection {* Class @{term term_of} *} class term_of = rtype + - constrains typ_of :: "'a\<Colon>{} itself \<Rightarrow> rtype" fixes term_of :: "'a \<Rightarrow> term" lemma term_of_anything: "term_of x \<equiv> t"