src/HOL/HOL.ML
changeset 2031 03a843f0f447
parent 1980 a22ff848be9b
child 2442 6663e0d210b0
--- a/src/HOL/HOL.ML	Thu Sep 26 11:11:22 1996 +0200
+++ b/src/HOL/HOL.ML	Thu Sep 26 12:47:47 1996 +0200
@@ -214,22 +214,22 @@
   [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
 
 qed_goal "contrapos2" HOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [
-	rtac classical 1,
-	dtac p2 1,
-	etac notE 1,
-	rtac p1 1]);
+        rtac classical 1,
+        dtac p2 1,
+        etac notE 1,
+        rtac p1 1]);
 
 qed_goal "swap2" HOL.thy "[| P;  Q ==> ~ P |] ==> ~ Q" (fn [p1,p2] => [
-	rtac notI 1,
-	dtac p2 1,
-	etac notE 1,
-	rtac p1 1]);
+        rtac notI 1,
+        dtac p2 1,
+        etac notE 1,
+        rtac p1 1]);
 
 (** Unique existence **)
 section "?!";
 
 qed_goalw "ex1I" HOL.thy [Ex1_def]
-	    "[| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
+            "[| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
  (fn prems =>
   [REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]);