equal
deleted
inserted
replaced
1692 |
1692 |
1693 declare equals_eq [symmetric, code post] |
1693 declare equals_eq [symmetric, code post] |
1694 |
1694 |
1695 end |
1695 end |
1696 |
1696 |
|
1697 hide (open) const eq |
|
1698 hide const eq |
|
1699 |
1697 setup {* |
1700 setup {* |
1698 Sign.hide_const true "HOL.eq" |
1701 CodeUnit.add_const_alias @{thm equals_eq} |
1699 #> CodeUnit.add_const_alias @{thm equals_eq} |
|
1700 *} |
1702 *} |
1701 |
1703 |
1702 lemma [code func]: |
1704 lemma [code func]: |
1703 shows "False \<and> x \<longleftrightarrow> False" |
1705 shows "False \<and> x \<longleftrightarrow> False" |
1704 and "True \<and> x \<longleftrightarrow> x" |
1706 and "True \<and> x \<longleftrightarrow> x" |