src/ZF/Trancl.ML
changeset 9211 6236c5285bd8
parent 8318 54d69141a17f
child 9907 473a6604da94
     1.1 --- a/src/ZF/Trancl.ML	Fri Jun 30 12:49:11 2000 +0200
     1.2 +++ b/src/ZF/Trancl.ML	Fri Jun 30 12:51:30 2000 +0200
     1.3 @@ -133,8 +133,7 @@
     1.4  qed "r_subset_trancl";
     1.5  
     1.6  (*intro rule by definition: from r^* and r  *)
     1.7 -Goalw [trancl_def]
     1.8 -    "!!r. [| <a,b> : r^*;  <b,c> : r |]   ==>  <a,c> : r^+";
     1.9 +Goalw [trancl_def] "[| <a,b> : r^*;  <b,c> : r |]   ==>  <a,c> : r^+";
    1.10  by (Blast_tac 1);
    1.11  qed "rtrancl_into_trancl1";
    1.12