# HG changeset patch
# User lcp
# Date 783682810 -3600
# Node ID dbb8431184f9d03f7d0039055af8c7c327e11bf6
# Parent  f304c8379e4d736a141cb7cedc25b8caf4b8ad8e
FOL/FOL/swap: deleted
FOL/FOL: tidied the signature

diff -r f304c8379e4d -r dbb8431184f9 src/FOL/FOL.ML
--- a/src/FOL/FOL.ML	Tue Nov 01 10:32:18 1994 +0100
+++ b/src/FOL/FOL.ML	Tue Nov 01 10:40:10 1994 +0100
@@ -10,15 +10,14 @@
 
 signature FOL_LEMMAS = 
   sig
-  val disjCI : thm
-  val excluded_middle : thm
-  val excluded_middle_tac : string -> int -> tactic
-  val exCI : thm
-  val ex_classical : thm
-  val iffCE : thm
-  val impCE : thm
-  val notnotD : thm
-  val swap : thm
+  val disjCI 		: thm
+  val excluded_middle 	: thm
+  val excluded_middle_tac: string -> int -> tactic
+  val exCI 		: thm
+  val ex_classical 	: thm
+  val iffCE 		: thm
+  val impCE 		: thm
+  val notnotD 		: thm
   end;
 
 
@@ -85,14 +84,6 @@
 	(etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);
 
 
-(*Should be used as swap since ~P becomes redundant*)
-val swap = prove_goal FOL.thy 
-   "~P ==> (~Q ==> P) ==> Q"
- (fn major::prems=>
-  [ (resolve_tac [classical] 1),
-    (rtac (major RS notE) 1),
-    (REPEAT (ares_tac prems 1)) ]);
-
 end;
 
 open FOL_Lemmas;