equal
deleted
inserted
replaced
92 by (case_tac "Suc n <= m" 2); |
92 by (case_tac "Suc n <= m" 2); |
93 by (auto_tac (claset(),simpset() addsimps |
93 by (auto_tac (claset(),simpset() addsimps |
94 [real_minus_add_distrib])); |
94 [real_minus_add_distrib])); |
95 qed "sumr_minus"; |
95 qed "sumr_minus"; |
96 |
96 |
97 context Arithmetic.thy; |
97 context NatArith.thy; |
98 |
98 |
99 Goal "!!n. ~ Suc n <= m + k ==> ~ Suc n <= m"; |
99 Goal "!!n. ~ Suc n <= m + k ==> ~ Suc n <= m"; |
100 by (auto_tac (claset() addSDs [not_leE],simpset())); |
100 by (auto_tac (claset() addSDs [not_leE],simpset())); |
101 qed "lemma_not_Suc_add"; |
101 qed "lemma_not_Suc_add"; |
102 |
102 |