# HG changeset patch
# User huffman
# Date 1159470073 -7200
# Node ID 807c5f7dcb94eb32b0288b25ff0641b524ececa2
# Parent  4aa5c89b933e994b6ccaeacafab662de00a210e0
rearranged axioms and simp rules for scaleR

diff -r 4aa5c89b933e -r 807c5f7dcb94 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Thu Sep 28 20:30:53 2006 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Thu Sep 28 21:01:13 2006 +0200
@@ -54,8 +54,8 @@
     by transfer (rule scaleR_right_distrib)
   show "\<And>x::'a star. (a + b) *# x = a *# x + b *# x"
     by transfer (rule scaleR_left_distrib)
-  show "\<And>x::'a star. (a * b) *# x = a *# b *# x"
-    by transfer (rule scaleR_assoc)
+  show "\<And>x::'a star. a *# b *# x = (a * b) *# x"
+    by transfer (rule scaleR_scaleR)
   show "\<And>x::'a star. 1 *# x = x"
     by transfer (rule scaleR_one)
 qed
@@ -92,7 +92,7 @@
 qed
 
 lemma Reals_eq_Standard: "(Reals :: hypreal set) = Standard"
-by (simp add: Reals_def Standard_def of_real_eq_star_of)
+by (simp add: Reals_def Standard_def)
 
 
 subsection{*Existence of Free Ultrafilter over the Naturals*}