equal
deleted
inserted
replaced
51 \ !!act s s'. \ |
51 \ !!act s s'. \ |
52 \ [| act : Acts; s : reachable(Init,Acts); P s; (s, s') : act |] \ |
52 \ [| act : Acts; s : reachable(Init,Acts); P s; (s, s') : act |] \ |
53 \ ==> P s' |] \ |
53 \ ==> P s' |] \ |
54 \ ==> P za"; |
54 \ ==> P za"; |
55 by (cut_facts_tac [major] 1); |
55 by (cut_facts_tac [major] 1); |
56 auto(); |
56 by Auto_tac; |
57 be traces.induct 1; |
57 be traces.induct 1; |
58 by (ALLGOALS (blast_tac (claset() addIs prems))); |
58 by (ALLGOALS (blast_tac (claset() addIs prems))); |
59 qed "reachable_induct"; |
59 qed "reachable_induct"; |
60 |
60 |
61 structure reachable = |
61 structure reachable = |