equal
deleted
inserted
replaced
133 |
133 |
134 |
134 |
135 subsubsection {* Code generator setup *} |
135 subsubsection {* Code generator setup *} |
136 |
136 |
137 lemmas [code func del] = term.recs term.cases term.size |
137 lemmas [code func del] = term.recs term.cases term.size |
138 lemma [code func, code func del]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" .. |
138 lemma [code func, code func del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" .. |
139 |
139 |
140 lemma [code func, code func del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" .. |
140 lemma [code func, code func del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" .. |
141 lemma [code func, code func del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" .. |
141 lemma [code func, code func del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" .. |
142 lemma [code func, code func del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" .. |
142 lemma [code func, code func del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" .. |
143 |
143 |