src/HOL/HOL.thy
changeset 45231 d85a2fdc586c
parent 45171 262f179665f9
child 45294 3c5d3d286055
     1.1 --- a/src/HOL/HOL.thy	Fri Oct 21 11:17:12 2011 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri Oct 21 11:17:14 2011 +0200
     1.3 @@ -1729,7 +1729,7 @@
     1.4    assumes equal_eq: "equal x y \<longleftrightarrow> x = y"
     1.5  begin
     1.6  
     1.7 -lemma equal [code_unfold, code_inline del]: "equal = (op =)"
     1.8 +lemma equal: "equal = (op =)"
     1.9    by (rule ext equal_eq)+
    1.10  
    1.11  lemma equal_refl: "equal x x \<longleftrightarrow> True"