src/Provers/classical.ML
changeset 18374 598e7fd7438b
parent 18223 20830cb4428c
child 18534 6799b38ed872
     1.1 --- a/src/Provers/classical.ML	Thu Dec 08 20:15:57 2005 +0100
     1.2 +++ b/src/Provers/classical.ML	Thu Dec 08 20:16:04 2005 +0100
     1.3 @@ -106,7 +106,6 @@
     1.4    val clarify_step_tac  : claset -> int -> tactic
     1.5    val step_tac          : claset -> int -> tactic
     1.6    val slow_step_tac     : claset -> int -> tactic
     1.7 -  val swap              : thm                 (* ~P ==> (~Q ==> P) ==> Q *)
     1.8    val swapify           : thm list -> thm list
     1.9    val swap_res_tac      : thm list -> int -> tactic
    1.10    val inst_step_tac     : claset -> int -> tactic
    1.11 @@ -135,6 +134,7 @@
    1.12  signature CLASSICAL =
    1.13  sig
    1.14    include BASIC_CLASSICAL
    1.15 +  val swap: thm  (* ~P ==> (~Q ==> P) ==> Q *)
    1.16    val add_context_safe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
    1.17    val del_context_safe_wrapper: string -> theory -> theory
    1.18    val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory