src/Provers/classical.ML
changeset 51718 c18cf90cb392
parent 51717 9e7d1c139569
child 51798 ad3a241def73
equal deleted inserted replaced
51717:9e7d1c139569 51718:c18cf90cb392
    55   val addSE2: Proof.context * (string * thm) -> Proof.context
    55   val addSE2: Proof.context * (string * thm) -> Proof.context
    56   val appSWrappers: Proof.context -> wrapper
    56   val appSWrappers: Proof.context -> wrapper
    57   val appWrappers: Proof.context -> wrapper
    57   val appWrappers: Proof.context -> wrapper
    58 
    58 
    59   val claset_of: Proof.context -> claset
    59   val claset_of: Proof.context -> claset
    60   val map_claset: (claset -> claset) -> Proof.context -> Proof.context
       
    61   val put_claset: claset -> Proof.context -> Proof.context
    60   val put_claset: claset -> Proof.context -> Proof.context
    62 
    61 
    63   val map_theory_claset: (Proof.context -> Proof.context) -> theory -> theory
    62   val map_theory_claset: (Proof.context -> Proof.context) -> theory -> theory
    64 
    63 
    65   val fast_tac: Proof.context -> int -> tactic
    64   val fast_tac: Proof.context -> int -> tactic