--- a/src/HOL/Real/RealDef.thy Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Real/RealDef.thy Thu Jan 04 10:23:01 2001 +0100
@@ -23,9 +23,10 @@
consts
"1r" :: real ("1r")
- (*Overloaded constant: denotes the Real subset of enclosing types such as
- hypreal and complex*)
- SReal :: "'a set"
+ (*Overloaded constants denoting the Nat and Real subsets of enclosing
+ types such as hypreal and complex*)
+ SNat, SReal :: "'a set"
+
defs
@@ -80,5 +81,6 @@
syntax (symbols)
SReal :: "'a set" ("\\<real>")
+ SNat :: "'a set" ("\\<nat>")
end