src/HOL/Lambda/Commutation.ML
changeset 3024 005d899b5c48
parent 2922 580647a879cf
child 3439 54785105178c
equal deleted inserted replaced
3023:01364e2f30ad 3024:005d899b5c48
    92  by (blast_tac (HOL_cs addIs
    92  by (blast_tac (HOL_cs addIs
    93       [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
    93       [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
    94        rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
    94        rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
    95 by (etac rtrancl_induct 1);
    95 by (etac rtrancl_induct 1);
    96  by (Blast_tac 1);
    96  by (Blast_tac 1);
    97 by (blast_tac (!claset delrules [rtrancl_refl] 
    97 by (Blast.depth_tac (!claset delrules [rtrancl_refl] 
    98                        addIs [r_into_rtrancl, rtrancl_trans]) 1);
    98                        addIs [r_into_rtrancl, rtrancl_trans]) 12 1);
    99 qed "Church_Rosser_confluent";
    99 qed "Church_Rosser_confluent";