equal
deleted
inserted
replaced
23 |
23 |
24 val [nat_case_0, nat_case_Suc] = thms "nat.cases"; |
24 val [nat_case_0, nat_case_Suc] = thms "nat.cases"; |
25 bind_thm ("nat_case_0", nat_case_0); |
25 bind_thm ("nat_case_0", nat_case_0); |
26 bind_thm ("nat_case_Suc", nat_case_Suc); |
26 bind_thm ("nat_case_Suc", nat_case_Suc); |
27 |
27 |
28 val LeastI = thm "LeastI"; |
|
29 val Least_Suc = thm "Least_Suc"; |
28 val Least_Suc = thm "Least_Suc"; |
30 val Least_Suc2 = thm "Least_Suc2"; |
29 val Least_Suc2 = thm "Least_Suc2"; |
31 val Least_le = thm "Least_le"; |
|
32 val One_nat_def = thm "One_nat_def"; |
30 val One_nat_def = thm "One_nat_def"; |
33 val Suc_Suc_eq = thm "Suc_Suc_eq"; |
31 val Suc_Suc_eq = thm "Suc_Suc_eq"; |
34 val Suc_def = thm "Suc_def"; |
32 val Suc_def = thm "Suc_def"; |
35 val Suc_diff_diff = thm "Suc_diff_diff"; |
33 val Suc_diff_diff = thm "Suc_diff_diff"; |
36 val Suc_diff_le = thm "Suc_diff_le"; |
34 val Suc_diff_le = thm "Suc_diff_le"; |
216 val not_add_less2 = thm "not_add_less2"; |
214 val not_add_less2 = thm "not_add_less2"; |
217 val not_gr0 = thm "not_gr0"; |
215 val not_gr0 = thm "not_gr0"; |
218 val not_leE = thm "not_leE"; |
216 val not_leE = thm "not_leE"; |
219 val not_le_iff_less = thm "not_le_iff_less"; |
217 val not_le_iff_less = thm "not_le_iff_less"; |
220 val not_less0 = thm "not_less0"; |
218 val not_less0 = thm "not_less0"; |
221 val not_less_Least = thm "not_less_Least"; |
|
222 val not_less_eq = thm "not_less_eq"; |
219 val not_less_eq = thm "not_less_eq"; |
223 val not_less_iff_le = thm "not_less_iff_le"; |
220 val not_less_iff_le = thm "not_less_iff_le"; |
224 val not_less_less_Suc_eq = thm "not_less_less_Suc_eq"; |
221 val not_less_less_Suc_eq = thm "not_less_less_Suc_eq"; |
225 val not_less_simps = thms "not_less_simps"; |
222 val not_less_simps = thms "not_less_simps"; |
226 val one_eq_mult_iff = thm "one_eq_mult_iff"; |
223 val one_eq_mult_iff = thm "one_eq_mult_iff"; |