# HG changeset patch
# User paulson
# Date 933678920 -7200
# Node ID 3a2f8fdf4dabe79e02167fa275ddd4ce49a3b042
# Parent  8737390d1d0afc6c2f70594b4802ed5f0b5f2f1e
added realT

diff -r 8737390d1d0a -r 3a2f8fdf4dab src/HOL/hologic.ML
--- 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 *)