equal
deleted
inserted
replaced
1727 class equal = |
1727 class equal = |
1728 fixes equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
1728 fixes equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
1729 assumes equal_eq: "equal x y \<longleftrightarrow> x = y" |
1729 assumes equal_eq: "equal x y \<longleftrightarrow> x = y" |
1730 begin |
1730 begin |
1731 |
1731 |
1732 lemma equal [code_unfold, code_inline del]: "equal = (op =)" |
1732 lemma equal: "equal = (op =)" |
1733 by (rule ext equal_eq)+ |
1733 by (rule ext equal_eq)+ |
1734 |
1734 |
1735 lemma equal_refl: "equal x x \<longleftrightarrow> True" |
1735 lemma equal_refl: "equal x x \<longleftrightarrow> True" |
1736 unfolding equal by rule+ |
1736 unfolding equal by rule+ |
1737 |
1737 |