equal
deleted
inserted
replaced
81 goal ParRed.thy "!t. s => t --> t => cd s"; |
81 goal ParRed.thy "!t. s => t --> t => cd s"; |
82 by (dB.induct_tac "s" 1); |
82 by (dB.induct_tac "s" 1); |
83 by (Simp_tac 1); |
83 by (Simp_tac 1); |
84 by (etac rev_mp 1); |
84 by (etac rev_mp 1); |
85 by (dB.induct_tac "dB1" 1); |
85 by (dB.induct_tac "dB1" 1); |
86 by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] addss !simpset))); |
86 by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] unsafe_addss (!simpset)))); |
87 qed_spec_mp "par_beta_cd"; |
87 qed_spec_mp "par_beta_cd"; |
88 |
88 |
89 (*** Confluence (via cd) ***) |
89 (*** Confluence (via cd) ***) |
90 |
90 |
91 goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)"; |
91 goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)"; |