src/HOL/SVC_Oracle.ML
changeset 7144 0feee8201d67
child 7162 8737390d1d0a
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SVC_Oracle.ML	Mon Aug 02 11:26:43 1999 +0200
     1.3 @@ -0,0 +1,23 @@
     1.4 +(*  Title:      HOL/SVC_Oracle
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson
     1.7 +    Copyright   1999  University of Cambridge
     1.8 +
     1.9 +Installing the oracle for SVC (Stanford Validity Checker)
    1.10 +
    1.11 +Based upon the work of Søren T. Heilmann
    1.12 +*)
    1.13 +
    1.14 +(*Present the entire subgoal to the oracle, assumptions and all, but possibly
    1.15 +  abstracted.  Use via compose_tac, which performs no lifting but will
    1.16 +  instantiate variables.*)
    1.17 +val svc_tac = SUBGOAL
    1.18 +  (fn (prem,i) => 
    1.19 +   let val (svc_prem, insts) = Svc.abstract prem
    1.20 +       val th = invoke_oracle thy "svc_oracle" 
    1.21 +	             (sign_of thy, Svc.OracleExn svc_prem)
    1.22 +
    1.23 +    in compose_tac (false, th, 0) i
    1.24 +    end handle Svc.OracleExn _ => no_tac);
    1.25 +
    1.26 +