equal
deleted
inserted
replaced
1090 assumes 1: "t = s" and 2: "u = t" |
1090 assumes 1: "t = s" and 2: "u = t" |
1091 shows "u = s" |
1091 shows "u = s" |
1092 using 2 1 by (rule trans) |
1092 using 2 1 by (rule trans) |
1093 |
1093 |
1094 use "arith_data.ML" |
1094 use "arith_data.ML" |
1095 setup arith_setup |
1095 declaration {* K arith_setup *} |
1096 |
1096 |
1097 text{*The following proofs may rely on the arithmetic proof procedures.*} |
1097 text{*The following proofs may rely on the arithmetic proof procedures.*} |
1098 |
1098 |
1099 lemma le_iff_add: "(m::nat) \<le> n = (\<exists>k. n = m + k)" |
1099 lemma le_iff_add: "(m::nat) \<le> n = (\<exists>k. n = m + k)" |
1100 by (auto simp: le_eq_less_or_eq dest: less_imp_Suc_add) |
1100 by (auto simp: le_eq_less_or_eq dest: less_imp_Suc_add) |