src/HOL/ex/SVC_Oracle.thy
author haftmann
Fri Jun 17 16:12:49 2005 +0200 (2005-06-17)
changeset 16417 9bc16273c2d4
parent 12869 f362c0323d92
child 16836 45a3dc4688bc
permissions -rw-r--r--
migrated theory headers to new format
     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 imports Main (** + Real??**)
    12 uses "svc_funcs.ML" begin
    13 
    14 consts
    15   (*reserved for the oracle*)
    16   iff_keep :: "[bool, bool] => bool"
    17   iff_unfold :: "[bool, bool] => bool"
    18 
    19 oracle
    20   svc_oracle = Svc.oracle
    21 
    22 end