src/HOL/ex/SVC_Oracle.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 17388 495c799df31d
child 20813 379ce56e5dc2
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     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