turned SVC_Oracle into a new-style theory in order to get automatic
handling of its additional dependency on Tools/svc_funcs.ML;
--- a/src/HOL/ROOT.ML Tue Aug 17 19:24:00 1999 +0200
+++ b/src/HOL/ROOT.ML Tue Aug 17 22:11:05 1999 +0200
@@ -75,9 +75,6 @@
use "bin_simprocs.ML";
cd "..";
-use "Tools/svc_funcs.ML";
-use_thy "SVC_Oracle";
-
(*the all-in-one theory*)
use_thy "Main";
--- a/src/HOL/SVC_Oracle.ML Tue Aug 17 19:24:00 1999 +0200
+++ b/src/HOL/SVC_Oracle.ML Tue Aug 17 22:11:05 1999 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/SVC_Oracle
+(* Title: HOL/SVC_Oracle.ML
ID: $Id$
Author: Lawrence C Paulson
Copyright 1999 University of Cambridge
@@ -11,9 +11,11 @@
(*Present the entire subgoal to the oracle, assumptions and all, but possibly
abstracted. Use via compose_tac, which performs no lifting but will
instantiate variables.*)
+local val svc_thy = the_context () in
+
fun svc_tac i st =
- let val prem = List.nth (prems_of st, i-1)
- val th = invoke_oracle thy "svc_oracle"
+ let val prem = BasisLibrary.List.nth (prems_of st, i-1)
+ val th = invoke_oracle svc_thy "svc_oracle"
(#sign (rep_thm st), Svc.OracleExn prem)
in
compose_tac (false, th, 0) i st
@@ -21,6 +23,8 @@
handle Svc.OracleExn _ => Seq.empty
| Subscript => Seq.empty;
+end;
+
(*True if SVC appears to exist*)
fun svc_enabled() = getenv "SVC_HOME" <> "";
--- 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