equal
deleted
inserted
replaced
50 val bexp2 = bexp_iff RS iffD2; |
50 val bexp2 = bexp_iff RS iffD2; |
51 |
51 |
52 goal Equiv.thy "!!c. <c,sigma> -c-> sigma' ==> <sigma,sigma'> : C(c)"; |
52 goal Equiv.thy "!!c. <c,sigma> -c-> sigma' ==> <sigma,sigma'> : C(c)"; |
53 |
53 |
54 (* start with rule induction *) |
54 (* start with rule induction *) |
55 by (etac (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1); |
55 by (etac evalc.induct 1); |
56 |
56 |
57 by (rewrite_tac (Gamma_def::C_rewrite_rules)); |
57 by (rewrite_tac (Gamma_def::C_rewrite_rules)); |
58 (* skip *) |
58 (* skip *) |
59 by (fast_tac comp_cs 1); |
59 by (fast_tac comp_cs 1); |
60 |
60 |