equal
deleted
inserted
replaced
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1998 TUM |
4 Copyright 1998 TUM |
5 *) |
5 *) |
6 |
6 |
7 Goal "steps A w O (eps A)^* = steps A w"; |
7 Goal "steps A w O (eps A)^* = steps A w"; |
8 by (exhaust_tac "w" 1); |
8 by (cases_tac "w" 1); |
9 by (ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc]))); |
9 by (ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc]))); |
10 qed_spec_mp "steps_epsclosure"; |
10 qed_spec_mp "steps_epsclosure"; |
11 Addsimps [steps_epsclosure]; |
11 Addsimps [steps_epsclosure]; |
12 |
12 |
13 Goal "[| (p,q) : (eps A)^*; (q,r) : steps A w |] ==> (p,r) : steps A w"; |
13 Goal "[| (p,q) : (eps A)^*; (q,r) : steps A w |] ==> (p,r) : steps A w"; |