| changeset 66148 | 5e60c2d0a1f1 |
| parent 61893 | 4121cc8479f8 |
| child 69597 | ff784d5a5bfb |
--- a/src/HOL/Unix/Nested_Environment.thy Tue Jun 20 13:07:45 2017 +0200 +++ b/src/HOL/Unix/Nested_Environment.thy Tue Jun 20 13:07:47 2017 +0200 @@ -522,9 +522,6 @@ subsection \<open>Code generation\<close> -lemma [code, code del]: - "(HOL.equal :: (_, _, _) env \<Rightarrow> _) = HOL.equal" .. - lemma equal_env_code [code]: fixes x y :: "'a::equal" and f g :: "'c::{equal, finite} \<Rightarrow> ('b::equal, 'a, 'c) env option"