equal
deleted
inserted
replaced
104 |
104 |
105 definition [code del]: |
105 definition [code del]: |
106 "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n" |
106 "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n" |
107 |
107 |
108 instance |
108 instance |
109 by (default, auto simp add: less_num_def less_eq_num_def num_eq_iff) |
109 by standard (auto simp add: less_num_def less_eq_num_def num_eq_iff) |
110 |
110 |
111 end |
111 end |
112 |
112 |
113 lemma nat_of_num_add: "nat_of_num (x + y) = nat_of_num x + nat_of_num y" |
113 lemma nat_of_num_add: "nat_of_num (x + y) = nat_of_num x + nat_of_num y" |
114 unfolding plus_num_def |
114 unfolding plus_num_def |