src/HOL/HOL.ML
changeset 3003 c5293a17afa6
parent 2562 d571d6660240
child 3436 d68dbb8f22d3
     1.1 --- a/src/HOL/HOL.ML	Mon Apr 21 11:19:28 1997 +0200
     1.2 +++ b/src/HOL/HOL.ML	Mon Apr 21 12:16:04 1997 +0200
     1.3 @@ -235,6 +235,12 @@
     1.4   (fn prems =>
     1.5    [REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]);
     1.6  
     1.7 +(*Sometimes easier to use: the premises have no shared variables.  Safe!*)
     1.8 +qed_goal "ex_ex1I" HOL.thy
     1.9 +    "[| ? x.P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> ?! x. P(x)"
    1.10 + (fn [ex,eq] => [ (rtac (ex RS exE) 1),
    1.11 +                  (REPEAT (ares_tac [ex1I,eq] 1)) ]);
    1.12 +
    1.13  qed_goalw "ex1E" HOL.thy [Ex1_def]
    1.14      "[| ?! x.P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R |] ==> R"
    1.15   (fn major::prems =>