| changeset 8442 | 96023903c2df |
| parent 8423 | 3c19160b6432 |
| child 10834 | a7897aebbffc |
--- a/src/HOL/Lex/NAe.ML Mon Mar 13 15:42:19 2000 +0100 +++ b/src/HOL/Lex/NAe.ML Mon Mar 13 16:23:34 2000 +0100 @@ -5,7 +5,7 @@ *) Goal "steps A w O (eps A)^* = steps A w"; -by (cases_tac "w" 1); +by (case_tac "w" 1); by (ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc]))); qed_spec_mp "steps_epsclosure"; Addsimps [steps_epsclosure];