src/HOL/ex/SVC_Oracle.thy
author wenzelm
Thu Jul 14 19:28:18 2005 +0200 (2005-07-14)
changeset 16836 45a3dc4688bc
parent 16417 9bc16273c2d4
child 17388 495c799df31d
permissions -rw-r--r--
improved oracle setup;
     1 (*  Title:      HOL/ex/SVC_Oracle.thy
     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 theory SVC_Oracle
    12 imports Main
    13 uses "svc_funcs.ML"
    14 begin
    15 
    16 consts
    17   iff_keep :: "[bool, bool] => bool"
    18   iff_unfold :: "[bool, bool] => bool"
    19 
    20 hide const iff_keep iff_unfold
    21 
    22 oracle
    23   svc_oracle ("term") = Svc.oracle
    24 
    25 end