equal
deleted
inserted
replaced
91 \ !!x y. [| finite y; x:y; P(y) |] ==> P(y-{x}) \ |
91 \ !!x y. [| finite y; x:y; P(y) |] ==> P(y-{x}) \ |
92 \ |] ==> c<=b --> P(b-c)"; |
92 \ |] ==> c<=b --> P(b-c)"; |
93 by (rtac (major RS finite_induct) 1); |
93 by (rtac (major RS finite_induct) 1); |
94 by (stac Diff_insert 2); |
94 by (stac Diff_insert 2); |
95 by (ALLGOALS (asm_simp_tac |
95 by (ALLGOALS (asm_simp_tac |
96 (simpset() addsimps (prems@[Diff_subset RS finite_subset])))); |
96 (simpset() addsimps prems@[Diff_subset RS finite_subset]))); |
97 val lemma = result(); |
97 val lemma = result(); |
98 |
98 |
99 val prems = Goal |
99 val prems = Goal |
100 "[| finite A; \ |
100 "[| finite A; \ |
101 \ P(A); \ |
101 \ P(A); \ |