# HG changeset patch
# User wenzelm
# Date 1134069364 -3600
# Node ID 598e7fd7438bd316364831b4dcb53c1ffe985d2e
# Parent  995cc683d95ccb028e0f349b3fc8dec01d8e29c0
swap: no longer pervasive;

diff -r 995cc683d95c -r 598e7fd7438b src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Thu Dec 08 20:15:57 2005 +0100
+++ b/src/HOL/cladata.ML	Thu Dec 08 20:16:04 2005 +0100
@@ -60,7 +60,6 @@
 structure BasicClassical: BASIC_CLASSICAL = Classical; 
 
 open BasicClassical;
-val swap = Library.swap;
 
 val _ = bind_thm ("contrapos_np", inst "Pa" "?Q" Classical.swap);
 
diff -r 995cc683d95c -r 598e7fd7438b src/Provers/classical.ML
--- a/src/Provers/classical.ML	Thu Dec 08 20:15:57 2005 +0100
+++ b/src/Provers/classical.ML	Thu Dec 08 20:16:04 2005 +0100
@@ -106,7 +106,6 @@
   val clarify_step_tac  : claset -> int -> tactic
   val step_tac          : claset -> int -> tactic
   val slow_step_tac     : claset -> int -> tactic
-  val swap              : thm                 (* ~P ==> (~Q ==> P) ==> Q *)
   val swapify           : thm list -> thm list
   val swap_res_tac      : thm list -> int -> tactic
   val inst_step_tac     : claset -> int -> tactic
@@ -135,6 +134,7 @@
 signature CLASSICAL =
 sig
   include BASIC_CLASSICAL
+  val swap: thm  (* ~P ==> (~Q ==> P) ==> Q *)
   val add_context_safe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
   val del_context_safe_wrapper: string -> theory -> theory
   val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory