--- a/src/HOL/Trancl.ML Fri Jan 07 11:04:15 2000 +0100
+++ b/src/HOL/Trancl.ML Fri Jan 07 11:06:03 2000 +0100
@@ -48,9 +48,9 @@
val major::prems = Goal
"[| (a,b) : r^*; \
-\ !!x. P((x,x)); \
-\ !!x y z.[| P((x,y)); (x,y): r^*; (y,z): r |] ==> P((x,z)) |] \
-\ ==> P((a,b))";
+\ !!x. P(x,x); \
+\ !!x y z.[| P(x,y); (x,y): r^*; (y,z): r |] ==> P(x,z) |] \
+\ ==> P(a,b)";
by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_induct) 1);
by (blast_tac (claset() addIs prems) 1);
qed "rtrancl_full_induct";