changeset 5537 | c2bd39a2c0ee |
parent 5516 | d80e9aeb4a2b |
child 5616 | 497eeeace3fc |
--- a/src/HOL/Finite.ML Wed Sep 23 10:11:18 1998 +0200 +++ b/src/HOL/Finite.ML Wed Sep 23 10:12:01 1998 +0200 @@ -93,7 +93,7 @@ by (rtac (major RS finite_induct) 1); by (stac Diff_insert 2); by (ALLGOALS (asm_simp_tac - (simpset() addsimps (prems@[Diff_subset RS finite_subset])))); + (simpset() addsimps prems@[Diff_subset RS finite_subset]))); val lemma = result(); val prems = Goal