equal
deleted
inserted
replaced
561 qed simp_all |
561 qed simp_all |
562 |
562 |
563 lemma [code nbe]: "HOL.equal (x :: (_, _, _) env) x \<longleftrightarrow> True" |
563 lemma [code nbe]: "HOL.equal (x :: (_, _, _) env) x \<longleftrightarrow> True" |
564 by (fact equal_refl) |
564 by (fact equal_refl) |
565 |
565 |
566 lemma [code, code del]: |
|
567 "(Code_Evaluation.term_of :: |
|
568 ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = |
|
569 Code_Evaluation.term_of" .. |
|
570 |
|
571 end |
566 end |