author | nipkow |
Tue, 02 Jan 2001 10:35:33 +0100 | |
changeset 10760 | 02d727c441bb |
parent 10759 | 994877ee68cb |
child 10761 | 0d36ace55e5a |
--- 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;