--- a/src/HOL/HOL.thy Thu Apr 03 23:55:11 2008 +0200
+++ b/src/HOL/HOL.thy Fri Apr 04 13:40:21 2008 +0200
@@ -1673,10 +1673,13 @@
lemma equals_eq [code inline, code func]: "op = \<equiv> eq"
by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq)
+declare equals_eq [symmetric, code post]
+
end
setup {*
- CodeUnit.add_const_alias @{thm equals_eq}
+ Sign.hide_names_i true ("const", ["HOL.eq"])
+ #> CodeUnit.add_const_alias @{thm equals_eq}
*}
lemma [code func]:
--- a/src/HOL/ex/NormalForm.thy Thu Apr 03 23:55:11 2008 +0200
+++ b/src/HOL/ex/NormalForm.thy Fri Apr 04 13:40:21 2008 +0200
@@ -8,8 +8,6 @@
imports Main "~~/src/HOL/Real/Rational"
begin
-declare equals_eq [symmetric, code post]
-
lemma "True" by normalization
lemma "p \<longrightarrow> True" by normalization
declare disj_assoc [code func]