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
wenzelm@12869
     1
(*  Title:      HOL/ex/SVC_Oracle.thy
wenzelm@12869
     2
    ID:         $Id$
wenzelm@12869
     3
    Author:     Lawrence C Paulson
wenzelm@12869
     4
    Copyright   1999  University of Cambridge
wenzelm@12869
     5
wenzelm@12869
     6
Installing the oracle for SVC (Stanford Validity Checker)
wenzelm@12869
     7
wenzelm@12869
     8
Based upon the work of SÝren T. Heilmann
wenzelm@12869
     9
*)
wenzelm@12869
    10
haftmann@16417
    11
theory SVC_Oracle imports Main (** + Real??**)
haftmann@16417
    12
uses "svc_funcs.ML" begin
wenzelm@12869
    13
wenzelm@12869
    14
consts
wenzelm@12869
    15
  (*reserved for the oracle*)
wenzelm@12869
    16
  iff_keep :: "[bool, bool] => bool"
wenzelm@12869
    17
  iff_unfold :: "[bool, bool] => bool"
wenzelm@12869
    18
wenzelm@12869
    19
oracle
wenzelm@12869
    20
  svc_oracle = Svc.oracle
wenzelm@12869
    21
wenzelm@12869
    22
end