Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Code_Evaluation.thy
changeset 38857 97775f3e8722
parent 38348 cf7b2121ad9d
child 39274 b17ffa965223
equal deleted inserted replaced
38856:168dba35ecf3 38857:97775f3e8722 
   160 
   160 
   161 
   161 
   162 subsubsection {* Code generator setup *}
 
   162 subsubsection {* Code generator setup *}
 
   163 
   163 
   164 lemmas [code del] = term.recs term.cases term.size
 
   164 lemmas [code del] = term.recs term.cases term.size
 
   165 lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
 
   165 lemma [code, code del]: "HOL.equal (t1\<Colon>term) t2 \<longleftrightarrow> HOL.equal t1 t2" ..
 
   166 
   166 
   167 lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
 
   167 lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
 
   168 lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
 
   168 lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
 
   169 lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" ..
 
   169 lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" ..
 
   170 lemma [code, code del]:
 
   170 lemma [code, code del]:
isabelle