# HG changeset patch
# User paulson
# Date 978516793 -3600
# Node ID 329d5f4aa43cc1098f63c4db52c9ccaf2bb58ee1
# Parent  08e1610c1dcb7220ad5e3ad9d3e3b82f4f3a49dd
some HOL-Real material

diff -r 08e1610c1dcb -r 329d5f4aa43c doc-src/TutorialI/Types/Numbers.thy
--- a/doc-src/TutorialI/Types/Numbers.thy	Tue Jan 02 22:41:17 2001 +0100
+++ b/doc-src/TutorialI/Types/Numbers.thy	Wed Jan 03 11:13:13 2001 +0100
@@ -1,5 +1,5 @@
 (* ID:         $Id$ *)
-theory Numbers = Main:
+theory Numbers = Real:
 
 ML "Pretty.setmargin 64"
 
@@ -167,13 +167,38 @@
 \rulename{abs_mult}
 *}  
 
-(*NO REALS YET;  Needs HOL-Real as parent
-For the reals, perhaps just a few results to indicate what is there.
+text {*REALS
+
+@{thm[display] realpow_abs[no_vars]}
+\rulename{realpow_abs}
+
+@{thm[display] real_dense[no_vars]}
+\rulename{real_dense}
 
 @{thm[display] realpow_abs[no_vars]}
 \rulename{realpow_abs}
 
-More once rinv (the most important constant) is sorted.
-*)  
+@{thm[display] real_times_divide1_eq[no_vars]}
+\rulename{real_times_divide1_eq}
+
+@{thm[display] real_times_divide2_eq[no_vars]}
+\rulename{real_times_divide2_eq}
+
+@{thm[display] real_divide_divide1_eq[no_vars]}
+\rulename{real_divide_divide1_eq}
+
+@{thm[display] real_divide_divide2_eq[no_vars]}
+\rulename{real_divide_divide2_eq}
+
+@{thm[display] real_minus_divide_eq[no_vars]}
+\rulename{real_minus_divide_eq}
+
+@{thm[display] real_divide_minus_eq[no_vars]}
+\rulename{real_divide_minus_eq}
+
+This last NOT a simprule
+
+real_add_divide_distrib
+*}
 
 end