the SVC oracle theory

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SVC_Oracle.ML	Mon Aug 02 11:26:43 1999 +0200
@@ -0,0 +1,23 @@
+(*  Title:      HOL/SVC_Oracle
+    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
+*)
+
+(*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.*)
+val svc_tac = SUBGOAL
+  (fn (prem,i) => 
+   let val (svc_prem, insts) = Svc.abstract prem
+       val th = invoke_oracle thy "svc_oracle" 
+	             (sign_of thy, Svc.OracleExn svc_prem)
+
+    in compose_tac (false, th, 0) i
+    end handle Svc.OracleExn _ => no_tac);
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SVC_Oracle.thy	Mon Aug 02 11:26:43 1999 +0200
@@ -0,0 +1,13 @@
+(*  Title:      HOL/SVC_Oracle
+    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
+*)
+
+SVC_Oracle = NatBin + (**Real?? + **)
+oracle svc_oracle = Svc.oracle
+end