changeset 15131 | c69542757a4d |
parent 15055 | aed573241bea |
child 15140 | 322485b816ac |
--- a/src/HOL/Real/PReal.thy Mon Aug 16 14:21:54 2004 +0200 +++ b/src/HOL/Real/PReal.thy Mon Aug 16 14:22:27 2004 +0200 @@ -7,7 +7,9 @@ provides some of the definitions. *) -theory PReal = Rational: +theory PReal +import Rational +begin text{*Could be generalized and moved to @{text Ring_and_Field}*} lemma add_eq_exists: "\<exists>x. a+x = (b::rat)"