# HG changeset patch
# User paulson
# Date 933586003 -7200
# Node ID 0feee8201d676e1e8e5c40a48caac44ac9fff86c
# Parent  9c02848c5404edf7445765c14ab25e2c3693e946
the SVC oracle theory

diff -r 9c02848c5404 -r 0feee8201d67 src/HOL/SVC_Oracle.ML
--- /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);
+
+
diff -r 9c02848c5404 -r 0feee8201d67 src/HOL/SVC_Oracle.thy
--- /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