--- a/src/HOL/SVC_Oracle.thy Tue Aug 17 19:24:00 1999 +0200
+++ b/src/HOL/SVC_Oracle.thy Tue Aug 17 22:11:05 1999 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/SVC_Oracle
+(* Title: HOL/SVC_Oracle.thy
ID: $Id$
Author: Lawrence C Paulson
Copyright 1999 University of Cambridge
@@ -8,11 +8,15 @@
Based upon the work of Søren T. Heilmann
*)
-SVC_Oracle = NatBin + (**Real?? + **)
+theory SVC_Oracle = NatBin (** + Real??**)
+files "Tools/svc_funcs.ML":
consts
(*reserved for the oracle*)
- iff_keep, iff_unfold :: [bool, bool] => bool
+ iff_keep :: "[bool, bool] => bool"
+ iff_unfold :: "[bool, bool] => bool"
-oracle svc_oracle = Svc.oracle
+oracle
+ svc_oracle = Svc.oracle
+
end