--- a/src/HOL/Hyperreal/HyperArith.thy Thu Sep 14 19:18:10 2006 +0200
+++ b/src/HOL/Hyperreal/HyperArith.thy Thu Sep 14 20:31:10 2006 +0200
@@ -104,29 +104,6 @@
*)
-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