cases: opaque by default;
fixed ML tactic: proper context;
added 'rename_tac', 'rename_tac';
--- a/src/Pure/Isar/method.ML Thu Aug 17 10:39:44 2000 +0200
+++ b/src/Pure/Isar/method.ML Thu Aug 17 10:40:31 2000 +0200
@@ -295,8 +295,8 @@
val resolveq_tac = gen_resolveq_tac Tactic.rtac;
-fun resolveq_cases_tac opaq = gen_resolveq_tac (fn (rule, cases) => fn i => fn st =>
- Seq.map (rpair (RuleCases.make opaq rule cases)) (Tactic.rtac rule i st));
+fun resolveq_cases_tac open_parms = gen_resolveq_tac (fn (rule, cases) => fn i => fn st =>
+ Seq.map (rpair (RuleCases.make open_parms rule cases)) (Tactic.rtac rule i st));
(* simple rule *)
@@ -376,13 +376,14 @@
fun set_tactic f = tactic_ref := f;
fun tactic txt ctxt = METHOD (fn facts =>
- (Context.use_mltext
- ("let fun tactic (ctxt: PureIsar.Proof.context) (facts: thm list) : tactic = \
- \let val thm = PureIsar.ProofContext.get_thm_closure ctxt\n\
- \ and thms = PureIsar.ProofContext.get_thms_closure ctxt in\n"
- ^ txt ^
- "\nend in PureIsar.Method.set_tactic tactic end")
- false (Some (ProofContext.theory_of ctxt)); ! tactic_ref ctxt facts));
+ (Context.use_mltext
+ ("let fun tactic (ctxt: PureIsar.Proof.context) (facts: thm list) : tactic = \
+ \let val thm = PureIsar.ProofContext.get_thm_closure ctxt\n\
+ \ and thms = PureIsar.ProofContext.get_thms_closure ctxt in\n"
+ ^ txt ^
+ "\nend in PureIsar.Method.set_tactic tactic end")
+ false None;
+ Context.setmp (Some (ProofContext.theory_of ctxt)) (! tactic_ref ctxt) facts));
@@ -615,6 +616,7 @@
val subgoal_meth = goal_args (Scan.repeat1 Args.name) Tactic.subgoals_tac;
val thin_meth = goal_args Args.name Tactic.thin_tac;
val rename_meth = goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac;
+val rotate_meth = goal_args (Scan.optional Args.int 1) Tactic.rotate_tac;
(* pure_methods *)
@@ -640,7 +642,8 @@
("cut_tac", inst_args cut_inst, "cut rule (dynamic instantiation!)"),
("subgoal_tac", subgoal_meth, "insert subgoal (dynamic instantiation!)"),
("thin_tac", thin_meth, "remove premise (dynamic instantiation!)"),
- ("rename_tac", rename_meth, "rename parameters (dynamic instantiation!)"),
+ ("rename_tac", rename_meth, "rename parameters of goal (dynamic instantiation!)"),
+ ("rotate_tac", rotate_meth, "rotate assumptions of goal"),
("prolog", thms_args prolog, "simple prolog interpreter"),
("tactic", simple_args Args.name tactic, "ML tactic as proof method")];