moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac

--- a/doc-src/HOL/HOL.tex	Mon Mar 23 19:01:15 2009 +0100
+++ b/doc-src/HOL/HOL.tex	Mon Mar 23 19:01:16 2009 +0100
@@ -1427,7 +1427,7 @@
 provides a decision procedure for \emph{linear arithmetic}: formulae involving
 addition and subtraction. The simplifier invokes a weak version of this
 decision procedure automatically. If this is not sufficent, you can invoke the
-full procedure \ttindex{arith_tac} explicitly.  It copes with arbitrary
+full procedure \ttindex{linear_arith_tac} explicitly.  It copes with arbitrary
 formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt-}, {\tt Suc}, {\tt
   min}, {\tt max} and numerical constants. Other subterms are treated as
 atomic, while subformulae not involving numerical types are ignored. Quantified
@@ -1438,10 +1438,10 @@
 If {\tt k} is a numeral, then {\tt div k}, {\tt mod k} and
 {\tt k dvd} are also supported. The former two are eliminated
 by case distinctions, again blowing up the running time.
-If the formula involves explicit quantifiers, \texttt{arith_tac} may take
+If the formula involves explicit quantifiers, \texttt{linear_arith_tac} may take
 super-exponential time and space.
 
-If \texttt{arith_tac} fails, try to find relevant arithmetic results in
+If \texttt{linear_arith_tac} fails, try to find relevant arithmetic results in
 the library.  The theories \texttt{Nat} and \texttt{NatArith} contain
 theorems about {\tt<}, {\tt<=}, \texttt{+}, \texttt{-} and \texttt{*}.
 Theory \texttt{Divides} contains theorems about \texttt{div} and

--- a/src/HOL/HoareParallel/OG_Examples.thy	Mon Mar 23 19:01:15 2009 +0100
+++ b/src/HOL/HoareParallel/OG_Examples.thy	Mon Mar 23 19:01:16 2009 +0100
@@ -443,7 +443,7 @@
 --{* 32 subgoals left *}
 apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
 
-apply(tactic {* TRYALL (simple_arith_tac @{context}) *})
+apply(tactic {* TRYALL (linear_arith_tac @{context}) *})
 --{* 9 subgoals left *}
 apply (force simp add:less_Suc_eq)
 apply(drule sym)

--- a/src/HOL/Nat.thy	Mon Mar 23 19:01:15 2009 +0100
+++ b/src/HOL/Nat.thy	Mon Mar 23 19:01:16 2009 +0100
@@ -63,9 +63,8 @@
 end
 
 lemma Suc_not_Zero: "Suc m \<noteq> 0"
-  apply (simp add: Zero_nat_def Suc_def Abs_Nat_inject [unfolded mem_def]
+  by (simp add: Zero_nat_def Suc_def Abs_Nat_inject [unfolded mem_def]
     Rep_Nat [unfolded mem_def] Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def])
-  done
 
 lemma Zero_not_Suc: "0 \<noteq> Suc m"
   by (rule not_sym, rule Suc_not_Zero not_sym)
@@ -82,7 +81,7 @@
   done
 
 lemma nat_induct [case_names 0 Suc, induct type: nat]:
-  -- {* for backward compatibility -- naming of variables differs *}
+  -- {* for backward compatibility -- names of variables differ *}
   fixes n
   assumes "P 0"
     and "\<And>n. P n \<Longrightarrow> P (Suc n)"
@@ -1345,19 +1344,13 @@
   shows "u = s"
   using 2 1 by (rule trans)
 
+setup Arith_Data.setup
+
 use "Tools/nat_arith.ML"
 declaration {* K Nat_Arith.setup *}
 
-ML{*
-structure ArithFacts =
-  NamedThmsFun(val name = "arith"
-               val description = "arith facts - only ground formulas");
-*}
-
-setup ArithFacts.setup
-
 use "Tools/lin_arith.ML"
-declaration {* K LinArith.setup *}
+declaration {* K Lin_Arith.setup *}
 
 lemmas [arith_split] = nat_diff_split split_min split_max
 

--- a/src/HOL/Presburger.thy	Mon Mar 23 19:01:15 2009 +0100
+++ b/src/HOL/Presburger.thy	Mon Mar 23 19:01:16 2009 +0100
@@ -439,12 +439,7 @@
 
 use "Tools/Qelim/presburger.ML"
 
-declaration {* fn _ =>
-  arith_tactic_add
-    (mk_arith_tactic "presburger" (fn ctxt => fn i => fn st =>
-       (warning "Trying Presburger arithmetic ...";   
-    Presburger.cooper_tac true [] [] ctxt i st)))
-*}
+setup {* Arith_Data.add_tactic "Presburger arithmetic" (K (Presburger.cooper_tac true [] [])) *}
 
 method_setup presburger = {*
 let

--- a/src/HOL/Tools/Qelim/cooper.ML	Mon Mar 23 19:01:15 2009 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Mar 23 19:01:16 2009 +0100
@@ -172,7 +172,7 @@
 
     (* Canonical linear form for terms, formulae etc.. *)
 fun provelin ctxt t = Goal.prove ctxt [] [] t 
-  (fn _ => EVERY [simp_tac lin_ss 1, TRY (simple_arith_tac ctxt 1)]);
+  (fn _ => EVERY [simp_tac lin_ss 1, TRY (linear_arith_tac ctxt 1)]);
 fun linear_cmul 0 tm = zero 
   | linear_cmul n tm = case tm of  
       Const (@{const_name HOL.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b

--- a/src/HOL/Tools/TFL/post.ML	Mon Mar 23 19:01:15 2009 +0100
+++ b/src/HOL/Tools/TFL/post.ML	Mon Mar 23 19:01:16 2009 +0100
@@ -55,7 +55,7 @@
   Prim.postprocess strict
    {wf_tac     = REPEAT (ares_tac wfs 1),
     terminator = asm_simp_tac ss 1
-                 THEN TRY (silent_arith_tac (Simplifier.the_context ss) 1 ORELSE
+                 THEN TRY (Arith_Data.arith_tac (Simplifier.the_context ss) 1 ORELSE
                            fast_tac (cs addSDs [@{thm not0_implies_Suc}] addss ss) 1),
     simplifier = Rules.simpl_conv ss []};
 

--- a/src/HOL/Tools/arith_data.ML	Mon Mar 23 19:01:15 2009 +0100
+++ b/src/HOL/Tools/arith_data.ML	Mon Mar 23 19:01:16 2009 +0100
@@ -6,6 +6,11 @@
 
 signature ARITH_DATA =
 sig
+  val arith_tac: Proof.context -> int -> tactic
+  val verbose_arith_tac: Proof.context -> int -> tactic
+  val add_tactic: string -> (bool -> Proof.context -> int -> tactic) -> theory -> theory
+  val get_arith_facts: Proof.context -> thm list
+
   val prove_conv_nohyps: tactic list -> Proof.context -> term * term -> thm option
   val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
   val prove_conv2: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
@@ -14,11 +19,54 @@
   val trans_tac: thm option -> tactic
   val prep_simproc: string * string list * (theory -> simpset -> term -> thm option)
     -> simproc
+
+  val setup: theory -> theory
 end;
 
 structure Arith_Data: ARITH_DATA =
 struct
 
+(* slots for pluging in arithmetic facts and tactics *)
+
+structure Arith_Facts = NamedThmsFun(
+  val name = "arith"
+  val description = "arith facts - only ground formulas"
+);
+
+val get_arith_facts = Arith_Facts.get;
+
+structure Arith_Tactics = TheoryDataFun
+(
+  type T = (serial * (string * (bool -> Proof.context -> int -> tactic))) list;
+  val empty = [];
+  val copy = I;
+  val extend = I;
+  fun merge _ = AList.merge (op =) (K true);
+);
+
+fun add_tactic name tac = Arith_Tactics.map (cons (serial (), (name, tac)));
+
+fun gen_arith_tac verbose ctxt =
+  let
+    val tactics = (Arith_Tactics.get o ProofContext.theory_of) ctxt
+    fun invoke (_, (name, tac)) k st = (if verbose
+      then warning ("Trying " ^ name ^ "...") else ();
+      tac verbose ctxt k st);
+  in FIRST' (map invoke (rev tactics)) end;
+
+val arith_tac = gen_arith_tac false;
+val verbose_arith_tac = gen_arith_tac true;
+
+val arith_method = Args.bang_facts >> (fn prems => fn ctxt =>
+  METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ get_arith_facts ctxt @ facts)
+    THEN' verbose_arith_tac ctxt)));
+
+val setup = Arith_Facts.setup
+  #> Method.setup @{binding arith} arith_method "various arithmetic decision procedures";
+
+
+(* various auxiliary and legacy *)
+
 fun prove_conv_nohyps tacs ctxt (t, u) =
   if t aconv u then NONE
   else let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))

--- a/src/HOL/Tools/function_package/scnp_reconstruct.ML	Mon Mar 23 19:01:15 2009 +0100
+++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML	Mon Mar 23 19:01:16 2009 +0100
@@ -197,7 +197,7 @@
               else if b <= a then @{thm pair_leqI2} else @{thm pair_leqI1}
           in
             rtac rule 1 THEN PRIMITIVE (Thm.elim_implies stored_thm)
-            THEN (if tag_flag then arith_tac ctxt 1 else all_tac)
+            THEN (if tag_flag then Arith_Data.verbose_arith_tac ctxt 1 else all_tac)
           end
 
         fun steps_tac MAX strict lq lp =

--- a/src/HOL/Tools/lin_arith.ML	Mon Mar 23 19:01:15 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Mon Mar 23 19:01:16 2009 +0100
@@ -6,13 +6,9 @@
 
 signature BASIC_LIN_ARITH =
 sig
-  type arith_tactic
-  val mk_arith_tactic: string -> (Proof.context -> int -> tactic) -> arith_tactic
-  val eq_arith_tactic: arith_tactic * arith_tactic -> bool
   val arith_split_add: attribute
   val arith_discrete: string -> Context.generic -> Context.generic
   val arith_inj_const: string * typ -> Context.generic -> Context.generic
-  val arith_tactic_add: arith_tactic -> Context.generic -> Context.generic
   val fast_arith_split_limit: int Config.T
   val fast_arith_neq_limit: int Config.T
   val lin_arith_pre_tac: Proof.context -> int -> tactic
@@ -21,9 +17,7 @@
   val trace_arith: bool ref
   val lin_arith_simproc: simpset -> term -> thm option
   val fast_nat_arith_simproc: simproc
-  val simple_arith_tac: Proof.context -> int -> tactic
-  val arith_tac: Proof.context -> int -> tactic
-  val silent_arith_tac: Proof.context -> int -> tactic
+  val linear_arith_tac: Proof.context -> int -> tactic
 end;
 
 signature LIN_ARITH =
@@ -39,7 +33,7 @@
   val setup: Context.generic -> Context.generic
 end;
 
-structure LinArith: LIN_ARITH =
+structure Lin_Arith: LIN_ARITH =
 struct
 
 (* Parameters data for general linear arithmetic functor *)
@@ -72,7 +66,7 @@
   let val _ $ t = Thm.prop_of thm
   in t = Const("False",HOLogic.boolT) end;
 
-fun is_nat(t) = fastype_of1 t = HOLogic.natT;
+fun is_nat t = (fastype_of1 t = HOLogic.natT);
 
 fun mk_nat_thm sg t =
   let val ct = cterm_of sg t  and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
@@ -83,49 +77,35 @@
 
 (* arith context data *)
 
-datatype arith_tactic =
-  ArithTactic of {name: string, tactic: Proof.context -> int -> tactic, id: stamp};
-
-fun mk_arith_tactic name tactic = ArithTactic {name = name, tactic = tactic, id = stamp ()};
-
-fun eq_arith_tactic (ArithTactic {id = id1, ...}, ArithTactic {id = id2, ...}) = (id1 = id2);
-
 structure ArithContextData = GenericDataFun
 (
   type T = {splits: thm list,
             inj_consts: (string * typ) list,
-            discrete: string list,
-            tactics: arith_tactic list};
-  val empty = {splits = [], inj_consts = [], discrete = [], tactics = []};
+            discrete: string list};
+  val empty = {splits = [], inj_consts = [], discrete = []};
   val extend = I;
   fun merge _
-   ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, tactics= tactics1},
-    {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, tactics= tactics2}) : T =
+   ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1},
+    {splits= splits2, inj_consts= inj_consts2, discrete= discrete2}) : T =
    {splits = Library.merge Thm.eq_thm_prop (splits1, splits2),
     inj_consts = Library.merge (op =) (inj_consts1, inj_consts2),
-    discrete = Library.merge (op =) (discrete1, discrete2),
-    tactics = Library.merge eq_arith_tactic (tactics1, tactics2)};
+    discrete = Library.merge (op =) (discrete1, discrete2)};
 );
 
 val get_arith_data = ArithContextData.get o Context.Proof;
 
 val arith_split_add = Thm.declaration_attribute (fn thm =>
-  ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
+  ArithContextData.map (fn {splits, inj_consts, discrete} =>
     {splits = update Thm.eq_thm_prop thm splits,
-     inj_consts = inj_consts, discrete = discrete, tactics = tactics}));
-
-fun arith_discrete d = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
-  {splits = splits, inj_consts = inj_consts,
-   discrete = update (op =) d discrete, tactics = tactics});
+     inj_consts = inj_consts, discrete = discrete}));
 
-fun arith_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
-  {splits = splits, inj_consts = update (op =) c inj_consts,
-   discrete = discrete, tactics= tactics});
+fun arith_discrete d = ArithContextData.map (fn {splits, inj_consts, discrete} =>
+  {splits = splits, inj_consts = inj_consts,
+   discrete = update (op =) d discrete});
 
-fun arith_tactic_add tac = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
-  {splits = splits, inj_consts = inj_consts, discrete = discrete,
-   tactics = update eq_arith_tactic tac tactics});
-
+fun arith_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete} =>
+  {splits = splits, inj_consts = update (op =) c inj_consts,
+   discrete = discrete});
 
 val (fast_arith_split_limit, setup1) = Attrib.config_int "fast_arith_split_limit" 9;
 val (fast_arith_neq_limit, setup2) = Attrib.config_int "fast_arith_neq_limit" 9;
@@ -794,7 +774,7 @@
    Most of the work is done by the cancel tactics. *)
 
 val init_arith_data =
- Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
+ map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
    {add_mono_thms = add_mono_thms @
     @{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field},
     mult_mono_thms = mult_mono_thms,
@@ -815,7 +795,7 @@
   arith_discrete "nat";
 
 fun add_arith_facts ss =
-  add_prems (ArithFacts.get (MetaSimplifier.the_context ss)) ss;
+  add_prems (Arith_Data.get_arith_facts (MetaSimplifier.the_context ss)) ss;
 
 val lin_arith_simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
 
@@ -895,27 +875,16 @@
     (REPEAT_DETERM o split_tac (#splits (get_arith_data ctxt)))
     (fast_ex_arith_tac ctxt ex);
 
-fun more_arith_tacs ctxt =
-  let val tactics = #tactics (get_arith_data ctxt)
-  in FIRST' (map (fn ArithTactic {tactic, ...} => tactic ctxt) tactics) end;
-
 in
 
-fun simple_arith_tac ctxt = FIRST' [fast_arith_tac ctxt,
-  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt true];
-
-fun arith_tac ctxt = FIRST' [fast_arith_tac ctxt,
-  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt true,
-  more_arith_tacs ctxt];
+fun gen_linear_arith_tac ex ctxt = FIRST' [fast_arith_tac ctxt,
+  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt ex];
 
-fun silent_arith_tac ctxt = FIRST' [fast_arith_tac ctxt,
-  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt false,
-  more_arith_tacs ctxt];
+val linear_arith_tac = gen_linear_arith_tac true;
 
-val arith_method = Args.bang_facts >>
-  (fn prems => fn ctxt => METHOD (fn facts =>
-      HEADGOAL (Method.insert_tac (prems @ ArithFacts.get ctxt @ facts)
-      THEN' arith_tac ctxt)));
+val linarith_method = Args.bang_facts >> (fn prems => fn ctxt =>
+  METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
+    THEN' linear_arith_tac ctxt)));
 
 end;
 
@@ -929,11 +898,12 @@
       (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))) #>
   Context.mapping
    (setup_options #>
-    Method.setup @{binding arith} arith_method "decide linear arithmetic" #>
+    Arith_Data.add_tactic "linear arithmetic" gen_linear_arith_tac #>
+    Method.setup @{binding linarith} linarith_method "linear arithmetic" #>
     Attrib.setup @{binding arith_split} (Scan.succeed arith_split_add)
       "declaration of split rules for arithmetic procedure") I;
 
 end;
 
-structure BasicLinArith: BASIC_LIN_ARITH = LinArith;
-open BasicLinArith;
+structure Basic_Lin_Arith: BASIC_LIN_ARITH = Lin_Arith;
+open Basic_Lin_Arith;

--- a/src/HOL/Word/WordArith.thy	Mon Mar 23 19:01:15 2009 +0100
+++ b/src/HOL/Word/WordArith.thy	Mon Mar 23 19:01:16 2009 +0100
@@ -512,7 +512,7 @@
 
 fun uint_arith_tacs ctxt = 
   let
-    fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty;
+    fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty;
     val cs = local_claset_of ctxt;
     val ss = local_simpset_of ctxt;
   in 
@@ -1075,7 +1075,7 @@
 
 fun unat_arith_tacs ctxt =   
   let
-    fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty;
+    fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty;
     val cs = local_claset_of ctxt;
     val ss = local_simpset_of ctxt;
   in 

--- a/src/HOL/ex/Arith_Examples.thy	Mon Mar 23 19:01:15 2009 +0100
+++ b/src/HOL/ex/Arith_Examples.thy	Mon Mar 23 19:01:16 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:  HOL/ex/Arith_Examples.thy
-    ID:     $Id$
     Author: Tjark Weber
 *)
 
@@ -14,13 +13,13 @@
 
   @{ML fast_arith_tac} is a very basic version of the tactic.  It performs no
   meta-to-object-logic conversion, and only some splitting of operators.
-  @{ML simple_arith_tac} performs meta-to-object-logic conversion, full
+  @{ML linear_arith_tac} performs meta-to-object-logic conversion, full
   splitting of operators, and NNF normalization of the goal.  The @{text arith}
   method combines them both, and tries other methods (e.g.~@{text presburger})
   as well.  This is the one that you should use in your proofs!
 
   An @{text arith}-based simproc is available as well (see @{ML
-  LinArith.lin_arith_simproc}), which---for performance
+  Lin_Arith.lin_arith_simproc}), which---for performance
   reasons---however does even less splitting than @{ML fast_arith_tac}
   at the moment (namely inequalities only).  (On the other hand, it
   does take apart conjunctions, which @{ML fast_arith_tac} currently
@@ -83,7 +82,7 @@
   by (tactic {* fast_arith_tac @{context} 1 *})
 
 lemma "!!x. ((x::nat) <= y) = (x - y = 0)"
-  by (tactic {* simple_arith_tac @{context} 1 *})
+  by (tactic {* linear_arith_tac @{context} 1 *})
 
 lemma "[| (x::nat) < y; d < 1 |] ==> x - y = d"
   by (tactic {* fast_arith_tac @{context} 1 *})
@@ -140,34 +139,34 @@
 subsection {* Meta-Logic *}
 
 lemma "x < Suc y == x <= y"
-  by (tactic {* simple_arith_tac @{context} 1 *})
+  by (tactic {* linear_arith_tac @{context} 1 *})
 
 lemma "((x::nat) == z ==> x ~= y) ==> x ~= y | z ~= y"
-  by (tactic {* simple_arith_tac @{context} 1 *})
+  by (tactic {* linear_arith_tac @{context} 1 *})
 
 
 subsection {* Various Other Examples *}
 
 lemma "(x < Suc y) = (x <= y)"
-  by (tactic {* simple_arith_tac @{context} 1 *})
+  by (tactic {* linear_arith_tac @{context} 1 *})
 
 lemma "[| (x::nat) < y; y < z |] ==> x < z"
   by (tactic {* fast_arith_tac @{context} 1 *})
 
 lemma "(x::nat) < y & y < z ==> x < z"
-  by (tactic {* simple_arith_tac @{context} 1 *})
+  by (tactic {* linear_arith_tac @{context} 1 *})
 
 text {* This example involves no arithmetic at all, but is solved by
   preprocessing (i.e. NNF normalization) alone. *}
 
 lemma "(P::bool) = Q ==> Q = P"
-  by (tactic {* simple_arith_tac @{context} 1 *})
+  by (tactic {* linear_arith_tac @{context} 1 *})
 
 lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> min (x::nat) y = 0"
-  by (tactic {* simple_arith_tac @{context} 1 *})
+  by (tactic {* linear_arith_tac @{context} 1 *})
 
 lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> max (x::nat) y = x + y"
-  by (tactic {* simple_arith_tac @{context} 1 *})
+  by (tactic {* linear_arith_tac @{context} 1 *})
 
 lemma "[| (x::nat) ~= y; a + 2 = b; a < y; y < b; a < x; x < b |] ==> False"
   by (tactic {* fast_arith_tac @{context} 1 *})
@@ -185,7 +184,7 @@
   by (tactic {* fast_arith_tac @{context} 1 *})
 
 lemma "[| (x::nat) < y; P (x - y) |] ==> P 0"
-  by (tactic {* simple_arith_tac @{context} 1 *})
+  by (tactic {* linear_arith_tac @{context} 1 *})
 
 lemma "(x - y) - (x::nat) = (x - x) - y"
   by (tactic {* fast_arith_tac @{context} 1 *})
@@ -207,7 +206,7 @@
 (*        preprocessing negates the goal and tries to compute its negation *)
 (*        normal form, which creates lots of separate cases for this       *)
 (*        disjunction of conjunctions                                      *)
-(* by (tactic {* simple_arith_tac 1 *}) *)
+(* by (tactic {* linear_arith_tac 1 *}) *)
 oops
 
 lemma "2 * (x::nat) ~= 1"