src/HOL/ex/SVC_Oracle.thy
author wenzelm
Sun Oct 01 18:29:32 2006 +0200 (2006-10-01)
changeset 20813 379ce56e5dc2
parent 17388 495c799df31d
child 24470 41c81e23c08d
permissions -rw-r--r--
proper use of svc_oracle.ML;
     1 (*  Title:      HOL/ex/SVC_Oracle.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson
     4     Copyright   1999  University of Cambridge
     5 
     6 Based upon the work of Søren T. Heilmann.
     7 *)
     8 
     9 header {* Installing an oracle for SVC (Stanford Validity Checker) *}
    10 
    11 theory SVC_Oracle
    12 imports Main
    13 uses "svc_funcs.ML" ("svc_oracle.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 use "svc_oracle.ML"
    26 
    27 end