equal
deleted
inserted
replaced
1140 |
1140 |
1141 declare "*.size" [noatp] |
1141 declare "*.size" [noatp] |
1142 |
1142 |
1143 |
1143 |
1144 subsection {* Code generator setup *} |
1144 subsection {* Code generator setup *} |
1145 |
|
1146 instance nat :: eq .. |
|
1147 |
|
1148 lemma [code func]: |
|
1149 "(0\<Colon>nat) = 0 \<longleftrightarrow> True" |
|
1150 "Suc n = Suc m \<longleftrightarrow> n = m" |
|
1151 "Suc n = 0 \<longleftrightarrow> False" |
|
1152 "0 = Suc m \<longleftrightarrow> False" |
|
1153 by auto |
|
1154 |
1145 |
1155 lemma [code func]: |
1146 lemma [code func]: |
1156 "(0\<Colon>nat) \<le> m \<longleftrightarrow> True" |
1147 "(0\<Colon>nat) \<le> m \<longleftrightarrow> True" |
1157 "Suc (n\<Colon>nat) \<le> m \<longleftrightarrow> n < m" |
1148 "Suc (n\<Colon>nat) \<le> m \<longleftrightarrow> n < m" |
1158 "(n\<Colon>nat) < 0 \<longleftrightarrow> False" |
1149 "(n\<Colon>nat) < 0 \<longleftrightarrow> False" |