--- a/src/HOL/SVC_Oracle.thy Tue Feb 05 15:51:28 2002 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(* Title: HOL/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 = NatBin (** + Real??**)
-files "Tools/svc_funcs.ML":
-
-consts
- (*reserved for the oracle*)
- iff_keep :: "[bool, bool] => bool"
- iff_unfold :: "[bool, bool] => bool"
-
-oracle
- svc_oracle = Svc.oracle
-
-end