*** empty log message ***

--- a/src/HOL/Real/real_arith0.ML	Tue Jan 02 10:27:10 2001 +0100
+++ b/src/HOL/Real/real_arith0.ML	Tue Jan 02 10:35:33 2001 +0100
@@ -71,6 +71,12 @@
   arith_discrete ("RealDef.real",false),
   Simplifier.change_simpset_of (op addsimprocs) [fast_real_arith_simproc]];
 
+(* some thms for injection nat => real:
+real_of_nat_zero
+zero_eq_numeral_0
+real_of_nat_add
+*)
+
 end;