changeset 6564 | c09997086ca7 |
parent 6536 | 281d44905cab |
child 6714 | 6b2b4ec58178 |
6563:128cf997c768 | 6564:c09997086ca7 |
---|---|
526 by (etac finite_induct 1); |
526 by (etac finite_induct 1); |
527 by (ALLGOALS Asm_simp_tac); |
527 by (ALLGOALS Asm_simp_tac); |
528 by (Clarify_tac 1); |
528 by (Clarify_tac 1); |
529 by (dtac ball_constrains_INT 1); |
529 by (dtac ball_constrains_INT 1); |
530 by (asm_full_simp_tac (simpset() addsimps [completion]) 1); |
530 by (asm_full_simp_tac (simpset() addsimps [completion]) 1); |
531 qed "finite_completion"; |
531 qed_spec_mp "finite_completion"; |
532 |
532 |