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