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