# HG changeset patch # User wenzelm # Date 933609546 -7200 # Node ID 687657a3f7e6145c1a38621d52451f2da68b0c2f # Parent 820c8c8573d9894d89e833175bfd9fb128b75a0c export cla_meth('); diff -r 820c8c8573d9 -r 687657a3f7e6 src/Provers/classical.ML --- a/src/Provers/classical.ML Mon Aug 02 17:58:46 1999 +0200 +++ b/src/Provers/classical.ML Mon Aug 02 17:59:06 1999 +0200 @@ -172,6 +172,8 @@ val xtra_intro_local: Proof.context attribute val delrule_local: Proof.context attribute val cla_modifiers: (Args.T list -> (Proof.context attribute * Args.T list)) list + val cla_meth: (claset -> tactic) -> Proof.context -> Proof.method + val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method val cla_method: (claset -> tactic) -> Args.src -> Proof.context -> Proof.method val cla_method': (claset -> int -> tactic) -> Args.src -> Proof.context -> Proof.method val single_tac: claset -> thm list -> int -> tactic