equal
deleted
inserted
replaced
128 |
128 |
129 (*Church-Rosser property for parallel contraction*) |
129 (*Church-Rosser property for parallel contraction*) |
130 goalw Comb.thy [diamond_def] "diamond parcontract"; |
130 goalw Comb.thy [diamond_def] "diamond parcontract"; |
131 by (rtac (impI RS allI RS allI) 1); |
131 by (rtac (impI RS allI RS allI) 1); |
132 by (etac parcontract.induct 1 THEN prune_params_tac); |
132 by (etac parcontract.induct 1 THEN prune_params_tac); |
133 by (Step_tac 1); |
133 by Safe_tac; |
134 by (ALLGOALS Blast_tac); |
134 by (ALLGOALS Blast_tac); |
135 qed "diamond_parcontract"; |
135 qed "diamond_parcontract"; |
136 |
136 |
137 |
137 |
138 (*** Equivalence of x--->y and x===>y ***) |
138 (*** Equivalence of x--->y and x===>y ***) |