author | haftmann |
Wed, 26 Feb 2014 11:57:55 +0100 | |
changeset 55758 | 385f7573f8f5 |
parent 55757 | 9fc71814b8c1 |
child 55759 | fe3d8f585c20 |
--- a/src/HOL/Unix/Nested_Environment.thy Wed Feb 26 11:57:52 2014 +0100 +++ b/src/HOL/Unix/Nested_Environment.thy Wed Feb 26 11:57:55 2014 +0100 @@ -563,9 +563,4 @@ lemma [code nbe]: "HOL.equal (x :: (_, _, _) env) x \<longleftrightarrow> True" by (fact equal_refl) -lemma [code, code del]: - "(Code_Evaluation.term_of :: - ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = - Code_Evaluation.term_of" .. - end