--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/SVC_Oracle.thy Tue Feb 05 23:18:08 2002 +0100
@@ -0,0 +1,22 @@
+(* Title: HOL/ex/SVC_Oracle.thy
+ ID: $Id$
+ Author: Lawrence C Paulson
+ Copyright 1999 University of Cambridge
+
+Installing the oracle for SVC (Stanford Validity Checker)
+
+Based upon the work of Søren T. Heilmann
+*)
+
+theory SVC_Oracle = Main (** + Real??**)
+files "svc_funcs.ML":
+
+consts
+ (*reserved for the oracle*)
+ iff_keep :: "[bool, bool] => bool"
+ iff_unfold :: "[bool, bool] => bool"
+
+oracle
+ svc_oracle = Svc.oracle
+
+end