# HG changeset patch # User wenzelm # Date 934920665 -7200 # Node ID 2919daadba912f8887681cf0432720d848512c3e # Parent e077484d50d89a8297bbbe7e6da9ac242c4ee690 turned SVC_Oracle into a new-style theory in order to get automatic handling of its additional dependency on Tools/svc_funcs.ML; diff -r e077484d50d8 -r 2919daadba91 src/HOL/ROOT.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"; diff -r e077484d50d8 -r 2919daadba91 src/HOL/SVC_Oracle.ML --- 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" <> ""; diff -r e077484d50d8 -r 2919daadba91 src/HOL/SVC_Oracle.thy --- 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