src/HOL/ex/SVC_Oracle.thy
author wenzelm
Sun Oct 01 18:29:32 2006 +0200 (2006-10-01)
changeset 20813 379ce56e5dc2
parent 17388 495c799df31d
child 24470 41c81e23c08d
permissions -rw-r--r--
proper use of svc_oracle.ML;
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@20813
    13
uses "svc_funcs.ML" ("svc_oracle.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@20813
    25
use "svc_oracle.ML"
wenzelm@20813
    26
wenzelm@12869
    27
end