src/HOL/ex/SVC_Oracle.thy
author wenzelm
Wed Sep 14 22:08:08 2005 +0200 (2005-09-14)
changeset 17388 495c799df31d
parent 16836 45a3dc4688bc
child 20813 379ce56e5dc2
permissions -rw-r--r--
tuned headers etc.;
     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"
    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