src/Provers/classical.ML
changeset 51688 27ecd33d3366
parent 51658 21c10672633b
child 51703 f2e92fc0c8aa
equal deleted inserted replaced
51687:3d8720271ebf 51688:27ecd33d3366
    54   val addSD2: claset * (string * thm) -> claset
    54   val addSD2: claset * (string * thm) -> claset
    55   val addSE2: claset * (string * thm) -> claset
    55   val addSE2: claset * (string * thm) -> claset
    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 global_claset_of: theory -> claset
       
    60   val claset_of: Proof.context -> claset
    59   val claset_of: Proof.context -> claset
    61   val map_claset: (claset -> claset) -> Proof.context -> Proof.context
    60   val map_claset: (claset -> claset) -> Proof.context -> Proof.context
    62   val put_claset: claset -> Proof.context -> Proof.context
    61   val put_claset: claset -> Proof.context -> Proof.context
    63 
    62 
    64   val fast_tac: Proof.context -> int -> tactic
    63   val fast_tac: Proof.context -> int -> tactic
   594   val empty = empty_cs;
   593   val empty = empty_cs;
   595   val extend = I;
   594   val extend = I;
   596   val merge = merge_cs;
   595   val merge = merge_cs;
   597 );
   596 );
   598 
   597 
   599 val global_claset_of = Claset.get o Context.Theory;
       
   600 val claset_of = Claset.get o Context.Proof;
   598 val claset_of = Claset.get o Context.Proof;
   601 val rep_claset_of = rep_cs o claset_of;
   599 val rep_claset_of = rep_cs o claset_of;
   602 
   600 
   603 val get_cs = Claset.get;
   601 val get_cs = Claset.get;
   604 val map_cs = Claset.map;
   602 val map_cs = Claset.map;