# HG changeset patch
# User nipkow
# Date 1127425435 -7200
# Node ID 760c6ade4ab615ac0b02fdf82c3718649434634c
# Parent  df8b2f0e462e07c3c6b2bb525d90e7b42da29711
renamed "rules" to "iprover"

diff -r df8b2f0e462e -r 760c6ade4ab6 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Sep 22 19:06:34 2005 +0200
+++ b/src/Pure/Isar/method.ML	Thu Sep 22 23:43:55 2005 +0200
@@ -50,7 +50,7 @@
   val erule: int -> thm list -> method
   val drule: int -> thm list -> method
   val frule: int -> thm list -> method
-  val rules_tac: ProofContext.context -> int option -> int -> tactic
+  val iprover_tac: ProofContext.context -> int option -> int -> tactic
   val bires_inst_tac: bool -> ProofContext.context -> (indexname * string) list ->
     thm -> int -> tactic
   val set_tactic: (ProofContext.context -> thm list -> tactic) -> unit
@@ -297,7 +297,7 @@
 end;
 
 
-(* rules -- intuitionistic proof search *)
+(* iprover -- intuitionistic proof search *)
 
 local
 
@@ -342,7 +342,7 @@
 
 in
 
-fun rules_tac ctxt opt_lim =
+fun iprover_tac ctxt opt_lim =
   SELECT_GOAL (DEEPEN (2, if_none opt_lim 20) (intprover_tac ctxt [] 0) 4 1);
 
 end;
@@ -658,7 +658,7 @@
 end;
 
 
-(* rules syntax *)
+(* iprover syntax *)
 
 local
 
@@ -671,7 +671,7 @@
   Args.$$$ name |-- (kind >> K NONE || kind' |-- Args.nat --| Args.colon >> SOME)
     >> (pair (I: ProofContext.context -> ProofContext.context) o att);
 
-val rules_modifiers =
+val iprover_modifiers =
  [modifier destN Args.bang_colon Args.bang ContextRules.dest_bang_local,
   modifier destN Args.colon (Scan.succeed ()) ContextRules.dest_local,
   modifier elimN Args.bang_colon Args.bang ContextRules.elim_bang_local,
@@ -682,10 +682,10 @@
 
 in
 
-fun rules_args m = bang_sectioned_args' rules_modifiers (Scan.lift (Scan.option Args.nat)) m;
+fun iprover_args m = bang_sectioned_args' iprover_modifiers (Scan.lift (Scan.option Args.nat)) m;
 
-fun rules_meth n prems ctxt = METHOD (fn facts =>
-  HEADGOAL (insert_tac (prems @ facts) THEN' ObjectLogic.atomize_tac THEN' rules_tac ctxt n));
+fun iprover_meth n prems ctxt = METHOD (fn facts =>
+  HEADGOAL (insert_tac (prems @ facts) THEN' ObjectLogic.atomize_tac THEN' iprover_tac ctxt n));
 
 end;
 
@@ -743,7 +743,7 @@
   ("fold", thms_args fold_meth, "fold definitions"),
   ("atomize", (atomize o #2) oo syntax (Args.mode "full"),
     "present local premises as object-level statements"),
-  ("rules", rules_args rules_meth, "apply many rules, including proof search"),
+  ("iprover", iprover_args iprover_meth, "intuitionistic proof search"),
   ("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"),
   ("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"),
   ("drule", nat_thms_args drule, "apply rule in destruct manner (improper)"),