# HG changeset patch
# User huffman
# Date 1158258670 -7200
# Node ID a7b2f90f698d1a0e6654efe6f63b94648ec3f0ea
# Parent  1c49d9f4410e52dbc7e6c3e8dfdcd8f80d082685
removed duplicate lemmas

diff -r 1c49d9f4410e -r a7b2f90f698d src/HOL/Hyperreal/HyperArith.thy
--- 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