src/HOL/Lambda/Commutation.thy
changeset 10179 9d5678e6bf34
parent 9811 39ffdb8cab03
child 10212 33fe2d701ddd
     1.1 --- a/src/HOL/Lambda/Commutation.thy	Mon Oct 09 19:20:55 2000 +0200
     1.2 +++ b/src/HOL/Lambda/Commutation.thy	Mon Oct 09 19:49:58 2000 +0200
     1.3 @@ -132,7 +132,7 @@
     1.4         rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD]) 1 *})
     1.5    apply (erule rtrancl_induct)
     1.6     apply blast
     1.7 -  apply (blast del: rtrancl_refl intro: r_into_rtrancl rtrancl_trans)
     1.8 +  apply (blast del: rtrancl_refl intro: rtranclIs)
     1.9    done
    1.10  
    1.11 -end
    1.12 \ No newline at end of file
    1.13 +end