equal
deleted
inserted
replaced
1816 |
1816 |
1817 code_datatype True False |
1817 code_datatype True False |
1818 |
1818 |
1819 code_datatype "TYPE('a\<Colon>{})" |
1819 code_datatype "TYPE('a\<Colon>{})" |
1820 |
1820 |
1821 code_datatype Trueprop "prop" |
1821 code_datatype "prop" Trueprop |
1822 |
1822 |
1823 text {* Code equations *} |
1823 text {* Code equations *} |
1824 |
1824 |
1825 lemma [code]: |
1825 lemma [code]: |
1826 shows "(False \<Longrightarrow> P) \<equiv> Trueprop True" |
1826 shows "(False \<Longrightarrow> P) \<equiv> Trueprop True" |