src/Provers/classical.ML
changeset 7154 687657a3f7e6
parent 7132 5c31d06ead04
child 7230 4ca0d7839ff1
equal deleted inserted replaced
7153:820c8c8573d9 7154:687657a3f7e6
   170   val xtra_dest_local: Proof.context attribute
   170   val xtra_dest_local: Proof.context attribute
   171   val xtra_elim_local: Proof.context attribute
   171   val xtra_elim_local: Proof.context attribute
   172   val xtra_intro_local: Proof.context attribute
   172   val xtra_intro_local: Proof.context attribute
   173   val delrule_local: Proof.context attribute
   173   val delrule_local: Proof.context attribute
   174   val cla_modifiers: (Args.T list -> (Proof.context attribute * Args.T list)) list
   174   val cla_modifiers: (Args.T list -> (Proof.context attribute * Args.T list)) list
       
   175   val cla_meth: (claset -> tactic) -> Proof.context -> Proof.method
       
   176   val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
   175   val cla_method: (claset -> tactic) -> Args.src -> Proof.context -> Proof.method
   177   val cla_method: (claset -> tactic) -> Args.src -> Proof.context -> Proof.method
   176   val cla_method': (claset -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
   178   val cla_method': (claset -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
   177   val single_tac: claset -> thm list -> int -> tactic
   179   val single_tac: claset -> thm list -> int -> tactic
   178   val setup: (theory -> theory) list
   180   val setup: (theory -> theory) list
   179 end;
   181 end;