| changeset 55642 | 63beb38e9258 |
| parent 52435 | 6646bb548c6b |
| child 56241 | 029246729dc0 |
--- a/src/HOL/Code_Evaluation.thy Fri Feb 21 00:09:55 2014 +0100 +++ b/src/HOL/Code_Evaluation.thy Fri Feb 21 00:09:56 2014 +0100 @@ -107,7 +107,7 @@ subsubsection {* Code generator setup *} -lemmas [code del] = term.recs term.cases term.size +lemmas [code del] = term.rec term.case term.size lemma [code, code del]: "HOL.equal (t1\<Colon>term) t2 \<longleftrightarrow> HOL.equal t1 t2" .. lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..