# HG changeset patch
# User paulson
# Date 933678538 -7200
# Node ID 8737390d1d0afc6c2f70594b4802ed5f0b5f2f1e
# Parent  7845a5cafbc68838aaf7c527347347bca10936a2
biconditionals and the natural numbers

diff -r 7845a5cafbc6 -r 8737390d1d0a src/HOL/SVC_Oracle.ML
--- a/src/HOL/SVC_Oracle.ML	Tue Aug 03 13:08:18 1999 +0200
+++ b/src/HOL/SVC_Oracle.ML	Tue Aug 03 13:08:58 1999 +0200
@@ -11,13 +11,14 @@
 (*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);
+fun svc_tac i st = 
+  let val prem = List.nth (prems_of st, i-1)
+      val th = invoke_oracle thy "svc_oracle" 
+	             (#sign (rep_thm st), Svc.OracleExn prem)
+   in 
+      compose_tac (false, th, 0) i st
+   end 
+   handle Svc.OracleExn _ => Seq.empty
+	| Subscript       => Seq.empty;
 
 
diff -r 7845a5cafbc6 -r 8737390d1d0a src/HOL/SVC_Oracle.thy
--- a/src/HOL/SVC_Oracle.thy	Tue Aug 03 13:08:18 1999 +0200
+++ b/src/HOL/SVC_Oracle.thy	Tue Aug 03 13:08:58 1999 +0200
@@ -9,5 +9,10 @@
 *)
 
 SVC_Oracle = NatBin + (**Real?? + **)
+
+consts
+  (*reserved for the oracle*)
+  iff_keep, iff_unfold :: [bool, bool] => bool 
+
 oracle svc_oracle = Svc.oracle
 end