# HG changeset patch
# User wenzelm
# Date 1190131534 -7200
# Node ID 0a3a020662444113dfe4beded4d5a992838c7db9
# Parent  779fc4fcbf8b1353c63800028292fe8e40fceda6
moved Tools/integer.ML to Pure/General/integer.ML;

diff -r 779fc4fcbf8b -r 0a3a02066244 NEWS
--- a/NEWS	Tue Sep 18 17:53:37 2007 +0200
+++ b/NEWS	Tue Sep 18 18:05:34 2007 +0200
@@ -1142,7 +1142,7 @@
 
 *** ML ***
 
-* Generic arithmetic modules: Tools/integer.ML, Tools/rat.ML, Tools/float.ML
+* Generic arithmetic modules: Tools/rat.ML, Tools/float.ML
 
 * Context data interfaces (Theory/Proof/GenericDataFun): removed
 name/print, uninitialized data defaults to ad-hoc copy of empty value,
diff -r 779fc4fcbf8b -r 0a3a02066244 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Sep 18 17:53:37 2007 +0200
+++ b/src/HOL/HOL.thy	Tue Sep 18 18:05:34 2007 +0200
@@ -8,7 +8,6 @@
 theory HOL
 imports CPure
 uses
-  "~~/src/Tools/integer.ML"
   ("hologic.ML")
   "~~/src/Tools/IsaPlanner/zipper.ML"
   "~~/src/Tools/IsaPlanner/isand.ML"
diff -r 779fc4fcbf8b -r 0a3a02066244 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Sep 18 17:53:37 2007 +0200
+++ b/src/HOL/IsaMakefile	Tue Sep 18 18:05:34 2007 +0200
@@ -83,7 +83,7 @@
   $(SRC)/Provers/induct_method.ML $(SRC)/Provers/order.ML		\
   $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML		\
   $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML			\
-  $(SRC)/Provers/trancl.ML $(SRC)/Tools/integer.ML $(SRC)/Tools/Metis/metis.ML\
+  $(SRC)/Provers/trancl.ML $(SRC)/Tools/Metis/metis.ML\
   $(SRC)/Tools/code/code_funcgr.ML			\
   $(SRC)/Tools/code/code_name.ML $(SRC)/Tools/code/code_package.ML		\
   $(SRC)/Tools/code/code_target.ML $(SRC)/Tools/code/code_thingol.ML	\
diff -r 779fc4fcbf8b -r 0a3a02066244 src/Pure/General/ROOT.ML
--- a/src/Pure/General/ROOT.ML	Tue Sep 18 17:53:37 2007 +0200
+++ b/src/Pure/General/ROOT.ML	Tue Sep 18 18:05:34 2007 +0200
@@ -16,6 +16,7 @@
 use "../ML/ml_parse.ML";
 use "secure.ML";
 
+use "integer.ML";
 use "stack.ML";
 use "heap.ML";
 use "ord_list.ML";
diff -r 779fc4fcbf8b -r 0a3a02066244 src/Pure/General/integer.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/integer.ML	Tue Sep 18 18:05:34 2007 +0200
@@ -0,0 +1,58 @@
+(*  Title:      Tools/integer.ML
+    ID:         $Id$
+    Author:     Florian Haftmann, TU Muenchen
+
+Unbounded integers.
+*)
+
+signature INTEGER =
+sig
+  val sign: int -> order
+  val sum: int list -> int
+  val div_mod: int -> int -> int * int
+  val square: int -> int
+  val pow: int -> int -> int (* exponent -> base -> result *)
+  val gcd: int -> int -> int
+  val gcds: int list -> int
+  val lcm: int -> int -> int
+  val lcms: int list -> int
+end;
+
+structure Integer : INTEGER =
+struct
+
+fun sign x = int_ord (x, 0);
+
+fun sum xs = fold (curry op +) xs 0;
+
+fun div_mod x y = IntInf.divMod (x, y);
+
+fun square x = x * x;
+
+fun pow k l =
+  let
+    fun pw 0 _ = 1
+      | pw 1 l = l
+      | pw k l =
+          let
+            val (k', r) = div_mod k 2;
+            val l' = pw k' (l * l);
+          in if r = 0 then l' else l' * l end;
+  in
+    if k < 0
+    then error "pow: negative exponent"
+    else pw k l
+  end;
+
+fun gcd x y =
+  let
+    fun gxd x y = if y = 0 then x else gxd y (x mod y)
+  in if x < y then gxd y x else gxd x y end;
+
+fun gcds xs = fold gcd xs 0;
+
+fun lcm x y = (x * y) div (gcd x y);
+fun lcms xs = fold lcm xs 1;
+
+end;
+
diff -r 779fc4fcbf8b -r 0a3a02066244 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue Sep 18 17:53:37 2007 +0200
+++ b/src/Pure/IsaMakefile	Tue Sep 18 18:05:34 2007 +0200
@@ -26,7 +26,7 @@
 $(OUT)/Pure$(ML_SUFFIX): \
   CPure.thy General/ROOT.ML General/alist.ML General/balanced_tree.ML		\
   General/basics.ML General/buffer.ML General/file.ML General/graph.ML		\
-  General/heap.ML General/history.ML General/markup.ML				\
+  General/heap.ML General/history.ML General/integer.ML General/markup.ML	\
   General/name_space.ML General/ord_list.ML General/output.ML			\
   General/path.ML General/position.ML General/pretty.ML				\
   General/print_mode.ML General/scan.ML General/secure.ML General/seq.ML	\
@@ -51,10 +51,10 @@
   ML-Systems/polyml-5.1.ML ML-Systems/polyml-interrupt-timeout.ML		\
   ML-Systems/polyml-old-basis.ML ML-Systems/polyml-posix.ML			\
   ML-Systems/polyml.ML ML-Systems/poplogml.ML ML-Systems/proper_int.ML		\
-  ML-Systems/smlnj.ML ML/ml_context.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML		\
-  Proof/extraction.ML Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML	\
-  Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/ROOT.ML		\
-  ProofGeneral/parsing.ML ProofGeneral/pgip.ML					\
+  ML-Systems/smlnj.ML ML/ml_context.ML ML/ml_lex.ML ML/ml_parse.ML		\
+  ML/ml_syntax.ML Proof/extraction.ML Proof/proof_rewrite_rules.ML		\
+  Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML		\
+  ProofGeneral/ROOT.ML ProofGeneral/parsing.ML ProofGeneral/pgip.ML		\
   ProofGeneral/pgip_input.ML ProofGeneral/pgip_isabelle.ML			\
   ProofGeneral/pgip_markup.ML ProofGeneral/pgip_output.ML			\
   ProofGeneral/pgip_parser.ML ProofGeneral/pgip_tests.ML			\
diff -r 779fc4fcbf8b -r 0a3a02066244 src/Tools/integer.ML
--- a/src/Tools/integer.ML	Tue Sep 18 17:53:37 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-(*  Title:      Tools/integer.ML
-    ID:         $Id$
-    Author:     Florian Haftmann, TU Muenchen
-
-Unbounded integers.
-*)
-
-signature INTEGER =
-sig
-  val sign: int -> order
-  val sum: int list -> int
-  val div_mod: int -> int -> int * int
-  val square: int -> int
-  val pow: int -> int -> int (* exponent -> base -> result *)
-  val gcd: int -> int -> int
-  val gcds: int list -> int
-  val lcm: int -> int -> int
-  val lcms: int list -> int
-end;
-
-structure Integer : INTEGER =
-struct
-
-fun sign x = int_ord (x, 0);
-
-fun sum xs = fold (curry op +) xs 0;
-
-fun div_mod x y = IntInf.divMod (x, y);
-
-fun square x = x * x;
-
-fun pow k l =
-  let
-    fun pw 0 _ = 1
-      | pw 1 l = l
-      | pw k l =
-          let
-            val (k', r) = div_mod k 2;
-            val l' = pw k' (l * l);
-          in if r = 0 then l' else l' * l end;
-  in
-    if k < 0
-    then error "pow: negative exponent"
-    else pw k l
-  end;
-
-fun gcd x y =
-  let
-    fun gxd x y = if y = 0 then x else gxd y (x mod y)
-  in if x < y then gxd y x else gxd x y end;
-
-fun gcds xs = fold gcd xs 0;
-
-fun lcm x y = (x * y) div (gcd x y);
-fun lcms xs = fold lcm xs 1;
-
-end;
-