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.;
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@17388
     6
Based upon the work of Søren T. Heilmann.
wenzelm@17388
     7
*)
wenzelm@12869
     8
wenzelm@17388
     9
header {* Installing an oracle for SVC (Stanford Validity Checker) *}
wenzelm@12869
    10
wenzelm@16836
    11
theory SVC_Oracle
wenzelm@16836
    12
imports Main
wenzelm@16836
    13
uses "svc_funcs.ML"
wenzelm@16836
    14
begin
wenzelm@12869
    15
wenzelm@12869
    16
consts
wenzelm@12869
    17
  iff_keep :: "[bool, bool] => bool"
wenzelm@12869
    18
  iff_unfold :: "[bool, bool] => bool"
wenzelm@12869
    19
wenzelm@16836
    20
hide const iff_keep iff_unfold
wenzelm@16836
    21
wenzelm@12869
    22
oracle
wenzelm@16836
    23
  svc_oracle ("term") = Svc.oracle
wenzelm@12869
    24
wenzelm@12869
    25
end