equal
deleted
inserted
replaced
1041 apply (fastsimp dest: mult_less_mono2) |
1041 apply (fastsimp dest: mult_less_mono2) |
1042 done |
1042 done |
1043 |
1043 |
1044 subsection {* Code generator setup *} |
1044 subsection {* Code generator setup *} |
1045 |
1045 |
|
1046 lemma one_is_suc_zero [code inline]: |
|
1047 "1 = Suc 0" |
|
1048 by simp |
|
1049 |
1046 code_alias |
1050 code_alias |
1047 "nat" "Nat.nat" |
1051 "nat" "Nat.nat" |
1048 "0" "Nat.Zero" |
1052 "0" "Nat.Zero" |
1049 "1" "Nat.One" |
1053 "1" "Nat.One" |
1050 "Suc" "Nat.Suc" |
1054 "Suc" "Nat.Suc" |