--- a/src/HOL/NSA/hypreal_arith.ML Mon Mar 23 19:01:15 2009 +0100
+++ b/src/HOL/NSA/hypreal_arith.ML Mon Mar 23 19:01:15 2009 +0100
@@ -30,10 +30,10 @@
Simplifier.simproc (the_context ())
"fast_hypreal_arith"
["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
- (K LinArith.lin_arith_simproc);
+ (K Lin_Arith.lin_arith_simproc);
val hypreal_arith_setup =
- LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
+ Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
{add_mono_thms = add_mono_thms,
mult_mono_thms = mult_mono_thms,
inj_thms = real_inj_thms @ inj_thms,
--- a/src/HOL/NatBin.thy Mon Mar 23 19:01:15 2009 +0100
+++ b/src/HOL/NatBin.thy Mon Mar 23 19:01:15 2009 +0100
@@ -651,7 +651,7 @@
val numeral_ss = @{simpset} addsimps @{thms numerals};
val nat_bin_arith_setup =
- LinArith.map_data
+ Lin_Arith.map_data
(fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
{add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
inj_thms = inj_thms,
--- a/src/HOL/Tools/int_arith.ML Mon Mar 23 19:01:15 2009 +0100
+++ b/src/HOL/Tools/int_arith.ML Mon Mar 23 19:01:15 2009 +0100
@@ -530,7 +530,7 @@
:: Int_Numeral_Simprocs.cancel_numerals;
val setup =
- LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
+ Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
{add_mono_thms = add_mono_thms,
mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
inj_thms = nat_inj_thms @ inj_thms,
@@ -547,7 +547,7 @@
"fast_int_arith"
["(m::'a::{ordered_idom,number_ring}) < n",
"(m::'a::{ordered_idom,number_ring}) <= n",
- "(m::'a::{ordered_idom,number_ring}) = n"] (K LinArith.lin_arith_simproc);
+ "(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.lin_arith_simproc);
end;
--- a/src/HOL/Tools/int_factor_simprocs.ML Mon Mar 23 19:01:15 2009 +0100
+++ b/src/HOL/Tools/int_factor_simprocs.ML Mon Mar 23 19:01:15 2009 +0100
@@ -232,7 +232,7 @@
val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT);
val pos = less $ zero $ t and neg = less $ t $ zero
fun prove p =
- Option.map Eq_True_elim (LinArith.lin_arith_simproc ss p)
+ Option.map Eq_True_elim (Lin_Arith.lin_arith_simproc ss p)
handle THM _ => NONE
in case prove pos of
SOME th => SOME(th RS pos_th)
--- a/src/HOL/Tools/nat_simprocs.ML Mon Mar 23 19:01:15 2009 +0100
+++ b/src/HOL/Tools/nat_simprocs.ML Mon Mar 23 19:01:15 2009 +0100
@@ -565,7 +565,7 @@
in
val nat_simprocs_setup =
- LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
+ Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
{add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
inj_thms = inj_thms, lessD = lessD, neqE = neqE,
simpset = simpset addsimps add_rules
--- a/src/HOL/Tools/rat_arith.ML Mon Mar 23 19:01:15 2009 +0100
+++ b/src/HOL/Tools/rat_arith.ML Mon Mar 23 19:01:15 2009 +0100
@@ -35,7 +35,7 @@
in
val rat_arith_setup =
- LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
+ Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
{add_mono_thms = add_mono_thms,
mult_mono_thms = mult_mono_thms,
inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
--- a/src/HOL/Tools/real_arith.ML Mon Mar 23 19:01:15 2009 +0100
+++ b/src/HOL/Tools/real_arith.ML Mon Mar 23 19:01:15 2009 +0100
@@ -29,7 +29,7 @@
in
val real_arith_setup =
- LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
+ Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
{add_mono_thms = add_mono_thms,
mult_mono_thms = mult_mono_thms,
inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,