src/HOL/SVC_Oracle.ML
author paulson
Fri Aug 06 17:28:45 1999 +0200 (1999-08-06)
changeset 7187 676027b1d770
parent 7162 8737390d1d0a
child 7237 2919daadba91
permissions -rw-r--r--
svc_enabled is now declared as a function
     1 (*  Title:      HOL/SVC_Oracle
     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 fun svc_tac i st = 
    15   let val prem = List.nth (prems_of st, i-1)
    16       val th = invoke_oracle thy "svc_oracle" 
    17 	             (#sign (rep_thm st), Svc.OracleExn prem)
    18    in 
    19       compose_tac (false, th, 0) i st
    20    end 
    21    handle Svc.OracleExn _ => Seq.empty
    22 	| Subscript       => Seq.empty;
    23 
    24 
    25 (*True if SVC appears to exist*)
    26 fun svc_enabled() = getenv "SVC_HOME" <> "";