src/HOL/SVC_Oracle.ML
author wenzelm
Tue Aug 17 22:11:05 1999 +0200 (1999-08-17)
changeset 7237 2919daadba91
parent 7187 676027b1d770
child 7284 29105299799c
permissions -rw-r--r--
turned SVC_Oracle into a new-style theory in order to get automatic
handling of its additional dependency on Tools/svc_funcs.ML;
     1 (*  Title:      HOL/SVC_Oracle.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson
     4     Copyright   1999  University of Cambridge
     5 
     6 Installing the oracle for SVC (Stanford Validity Checker)
     7 
     8 Based upon the work of Søren T. Heilmann
     9 *)
    10 
    11 (*Present the entire subgoal to the oracle, assumptions and all, but possibly
    12   abstracted.  Use via compose_tac, which performs no lifting but will
    13   instantiate variables.*)
    14 local val svc_thy = the_context () in
    15 
    16 fun svc_tac i st = 
    17   let val prem = BasisLibrary.List.nth (prems_of st, i-1)
    18       val th = invoke_oracle svc_thy "svc_oracle"
    19 	             (#sign (rep_thm st), Svc.OracleExn prem)
    20    in 
    21       compose_tac (false, th, 0) i st
    22    end 
    23    handle Svc.OracleExn _ => Seq.empty
    24 	| Subscript       => Seq.empty;
    25 
    26 end;
    27 
    28 
    29 (*True if SVC appears to exist*)
    30 fun svc_enabled() = getenv "SVC_HOME" <> "";