--- a/src/HOL/Hyperreal/HyperArith.thy Sat Jul 29 00:51:36 2006 +0200
+++ b/src/HOL/Hyperreal/HyperArith.thy Sat Jul 29 13:15:12 2006 +0200
@@ -11,12 +11,6 @@
uses ("hypreal_arith.ML")
begin
-subsection{*Numerals and Arithmetic*}
-
-use "hypreal_arith.ML"
-
-setup hypreal_arith_setup
-
subsection{*Absolute Value Function for the Hyperreals*}
lemma hrabs_add_less:
@@ -109,4 +103,32 @@
Addsimps [symmetric hypreal_diff_def]
*)
+
+subsection{*Numerals and Arithmetic*}
+
+lemma star_of_zero: "star_of 0 = 0"
+ by simp
+
+lemma star_of_one: "star_of 1 = 1"
+ by simp
+
+lemma star_of_add: "star_of (x + y) = star_of x + star_of y"
+ by simp
+
+lemma star_of_minus: "star_of (- x) = - star_of x"
+ by simp
+
+lemma star_of_diff: "star_of (x - y) = star_of x - star_of y"
+ by simp
+
+lemma star_of_mult: "star_of (x * y) = star_of x * star_of y"
+ by simp
+
+lemma star_of_number_of: "star_of (number_of v) = number_of v"
+ by simp
+
+use "hypreal_arith.ML"
+
+setup hypreal_arith_setup
+
end