structure LinArith now named Lin_Arith
authorhaftmann
Mon Mar 23 19:01:15 2009 +0100 (2009-03-23)
changeset 30685dd5fe091ff04
parent 30684 c98a64746c69
child 30686 47a32dd1b86e
structure LinArith now named Lin_Arith
src/HOL/NSA/hypreal_arith.ML
src/HOL/NatBin.thy
src/HOL/Tools/int_arith.ML
src/HOL/Tools/int_factor_simprocs.ML
src/HOL/Tools/nat_simprocs.ML
src/HOL/Tools/rat_arith.ML
src/HOL/Tools/real_arith.ML
     1.1 --- a/src/HOL/NSA/hypreal_arith.ML	Mon Mar 23 19:01:15 2009 +0100
     1.2 +++ b/src/HOL/NSA/hypreal_arith.ML	Mon Mar 23 19:01:15 2009 +0100
     1.3 @@ -30,10 +30,10 @@
     1.4      Simplifier.simproc (the_context ())
     1.5        "fast_hypreal_arith" 
     1.6        ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
     1.7 -    (K LinArith.lin_arith_simproc);
     1.8 +    (K Lin_Arith.lin_arith_simproc);
     1.9  
    1.10  val hypreal_arith_setup =
    1.11 -  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    1.12 +  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    1.13     {add_mono_thms = add_mono_thms,
    1.14      mult_mono_thms = mult_mono_thms,
    1.15      inj_thms = real_inj_thms @ inj_thms,
     2.1 --- a/src/HOL/NatBin.thy	Mon Mar 23 19:01:15 2009 +0100
     2.2 +++ b/src/HOL/NatBin.thy	Mon Mar 23 19:01:15 2009 +0100
     2.3 @@ -651,7 +651,7 @@
     2.4  val numeral_ss = @{simpset} addsimps @{thms numerals};
     2.5  
     2.6  val nat_bin_arith_setup =
     2.7 - LinArith.map_data
     2.8 + Lin_Arith.map_data
     2.9     (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    2.10       {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
    2.11        inj_thms = inj_thms,
     3.1 --- a/src/HOL/Tools/int_arith.ML	Mon Mar 23 19:01:15 2009 +0100
     3.2 +++ b/src/HOL/Tools/int_arith.ML	Mon Mar 23 19:01:15 2009 +0100
     3.3 @@ -530,7 +530,7 @@
     3.4    :: Int_Numeral_Simprocs.cancel_numerals;
     3.5  
     3.6  val setup =
     3.7 -  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     3.8 +  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     3.9     {add_mono_thms = add_mono_thms,
    3.10      mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
    3.11      inj_thms = nat_inj_thms @ inj_thms,
    3.12 @@ -547,7 +547,7 @@
    3.13    "fast_int_arith" 
    3.14       ["(m::'a::{ordered_idom,number_ring}) < n",
    3.15        "(m::'a::{ordered_idom,number_ring}) <= n",
    3.16 -      "(m::'a::{ordered_idom,number_ring}) = n"] (K LinArith.lin_arith_simproc);
    3.17 +      "(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.lin_arith_simproc);
    3.18  
    3.19  end;
    3.20  
     4.1 --- a/src/HOL/Tools/int_factor_simprocs.ML	Mon Mar 23 19:01:15 2009 +0100
     4.2 +++ b/src/HOL/Tools/int_factor_simprocs.ML	Mon Mar 23 19:01:15 2009 +0100
     4.3 @@ -232,7 +232,7 @@
     4.4        val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT);
     4.5        val pos = less $ zero $ t and neg = less $ t $ zero
     4.6        fun prove p =
     4.7 -        Option.map Eq_True_elim (LinArith.lin_arith_simproc ss p)
     4.8 +        Option.map Eq_True_elim (Lin_Arith.lin_arith_simproc ss p)
     4.9          handle THM _ => NONE
    4.10      in case prove pos of
    4.11           SOME th => SOME(th RS pos_th)
     5.1 --- a/src/HOL/Tools/nat_simprocs.ML	Mon Mar 23 19:01:15 2009 +0100
     5.2 +++ b/src/HOL/Tools/nat_simprocs.ML	Mon Mar 23 19:01:15 2009 +0100
     5.3 @@ -565,7 +565,7 @@
     5.4  in
     5.5  
     5.6  val nat_simprocs_setup =
     5.7 -  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     5.8 +  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     5.9     {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
    5.10      inj_thms = inj_thms, lessD = lessD, neqE = neqE,
    5.11      simpset = simpset addsimps add_rules
     6.1 --- a/src/HOL/Tools/rat_arith.ML	Mon Mar 23 19:01:15 2009 +0100
     6.2 +++ b/src/HOL/Tools/rat_arith.ML	Mon Mar 23 19:01:15 2009 +0100
     6.3 @@ -35,7 +35,7 @@
     6.4  in
     6.5  
     6.6  val rat_arith_setup =
     6.7 -  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     6.8 +  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     6.9     {add_mono_thms = add_mono_thms,
    6.10      mult_mono_thms = mult_mono_thms,
    6.11      inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
     7.1 --- a/src/HOL/Tools/real_arith.ML	Mon Mar 23 19:01:15 2009 +0100
     7.2 +++ b/src/HOL/Tools/real_arith.ML	Mon Mar 23 19:01:15 2009 +0100
     7.3 @@ -29,7 +29,7 @@
     7.4  in
     7.5  
     7.6  val real_arith_setup =
     7.7 -  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     7.8 +  Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     7.9     {add_mono_thms = add_mono_thms,
    7.10      mult_mono_thms = mult_mono_thms,
    7.11      inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,