added realT

--- a/src/HOL/hologic.ML	Tue Aug 03 13:08:58 1999 +0200
+++ b/src/HOL/hologic.ML	Tue Aug 03 13:15:20 1999 +0200
@@ -55,6 +55,7 @@
   val mk_nat: int -> term
   val dest_nat: term -> int
   val intT: typ
+  val realT: typ
   val binT: typ
   val pls_const: term
   val min_const: term
@@ -218,6 +219,8 @@
 
 val intT = Type ("IntDef.int", []);
 
+val realT = Type("RealDef.real",[]);
+
 
 (* binary numerals *)