src/HOL/Relation.ML
changeset 3718 d78cf498a88c
parent 3439 54785105178c
child 4089 96fba19bcbe2
     1.1 --- a/src/HOL/Relation.ML	Fri Sep 26 10:12:04 1997 +0200
     1.2 +++ b/src/HOL/Relation.ML	Fri Sep 26 10:21:14 1997 +0200
     1.3 @@ -164,7 +164,7 @@
     1.4      "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P"
     1.5   (fn major::prems=>
     1.6    [ (rtac (major RS CollectE) 1),
     1.7 -    (Step_tac 1),
     1.8 +    (Clarify_tac 1),
     1.9      (rtac (hd prems) 1),
    1.10      (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
    1.11