# HG changeset patch # User wenzelm # Date 1164811499 -3600 # Node ID 8831206d7f419480209cb8597faa76e50953fbbc # Parent 5e0f2340caa7cca2113016f844af75b2a3800404 renamed SIMPLE_METHOD' to SIMPLE_METHOD''; added simple version of SIMPLE_METHOD'; diff -r 5e0f2340caa7 -r 8831206d7f41 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Wed Nov 29 15:44:58 2006 +0100 +++ b/src/Pure/Isar/method.ML Wed Nov 29 15:44:59 2006 +0100 @@ -29,7 +29,8 @@ val insert: thm list -> method val insert_facts: method val SIMPLE_METHOD: tactic -> method - val SIMPLE_METHOD': ((int -> tactic) -> tactic) -> (int -> tactic) -> method + val SIMPLE_METHOD': (int -> tactic) -> method + val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method val defer: int option -> method val prefer: int -> method val cheating: bool -> Proof.context -> method @@ -163,7 +164,8 @@ fun insert thms = METHOD (fn _ => ALLGOALS (insert_tac thms)); fun SIMPLE_METHOD tac = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN tac); -fun SIMPLE_METHOD' quant tac = METHOD (fn facts => quant (insert_tac facts THEN' tac)); +fun SIMPLE_METHOD'' quant tac = METHOD (fn facts => quant (insert_tac facts THEN' tac)); +val SIMPLE_METHOD' = SIMPLE_METHOD'' HEADGOAL; end; @@ -182,8 +184,8 @@ (* unfold intro/elim rules *) -fun intro ths = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.match_tac ths)); -fun elim ths = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.ematch_tac ths)); +fun intro ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.match_tac ths)); +fun elim ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.ematch_tac ths)); (* unfold/fold definitions *) @@ -194,7 +196,7 @@ (* atomize rule statements *) -fun atomize false = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o ObjectLogic.atomize_tac) +fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o ObjectLogic.atomize_tac) | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o ObjectLogic.full_atomize_tac))); @@ -205,8 +207,8 @@ (* fact -- composition by facts from context *) -fun fact [] ctxt = SIMPLE_METHOD' HEADGOAL (ProofContext.some_fact_tac ctxt) - | fact rules _ = SIMPLE_METHOD' HEADGOAL (ProofContext.fact_tac rules); +fun fact [] ctxt = SIMPLE_METHOD' (ProofContext.some_fact_tac ctxt) + | fact rules _ = SIMPLE_METHOD' (ProofContext.fact_tac rules); (* assumption *) @@ -538,13 +540,13 @@ (#2 oo syntax (Scan.lift (Scan.optional (Args.parens Args.nat) 0) -- Attrib.thms)); fun goal_args' args tac src ctxt = #2 (syntax (Args.goal_spec HEADGOAL -- args >> - (fn (quant, s) => SIMPLE_METHOD' quant (tac s))) src ctxt); + (fn (quant, s) => SIMPLE_METHOD'' quant (tac s))) src ctxt); fun goal_args args tac = goal_args' (Scan.lift args) tac; fun goal_args_ctxt' args tac src ctxt = #2 (syntax (Args.goal_spec HEADGOAL -- args >> - (fn (quant, s) => SIMPLE_METHOD' quant (tac ctxt s))) src ctxt); + (fn (quant, s) => SIMPLE_METHOD'' quant (tac ctxt s))) src ctxt); fun goal_args_ctxt args tac = goal_args_ctxt' (Scan.lift args) tac;