# HG changeset patch
# User nipkow
# Date 978428133 -3600
# Node ID 02d727c441bb620c5810d793d2fc0c134936cf14
# Parent  994877ee68cbd86bb2b93fdcfc0aa819278d2c97
*** empty log message ***

diff -r 994877ee68cb -r 02d727c441bb src/HOL/Real/real_arith0.ML
--- 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;