src/HOL/Wellfounded.thy
changeset 47433 07f4bf913230
parent 46883 eec472dae593
child 48891 c0eafbd55de3
     1.1 --- a/src/HOL/Wellfounded.thy	Tue Apr 03 08:55:06 2012 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Tue Apr 03 17:26:30 2012 +0900
     1.3 @@ -271,7 +271,7 @@
     1.4        assume "y \<in> Q"
     1.5        with `y \<notin> ?Q'` 
     1.6        obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto
     1.7 -      from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> R O S" by (rule rel_compI)
     1.8 +      from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> R O S" by (rule relcompI)
     1.9        with `R O S \<subseteq> R` have "(w, z) \<in> R" ..
    1.10        with `z \<in> ?Q'` have "w \<notin> Q" by blast 
    1.11        with `w \<in> Q` show False by contradiction