src/HOL/SVC_Oracle.thy
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 7237 2919daadba91
permissions -rw-r--r--
improved theory reference in comment
wenzelm@7237
     1
(*  Title:      HOL/SVC_Oracle.thy
paulson@7144
     2
    ID:         $Id$
paulson@7144
     3
    Author:     Lawrence C Paulson
paulson@7144
     4
    Copyright   1999  University of Cambridge
paulson@7144
     5
paulson@7144
     6
Installing the oracle for SVC (Stanford Validity Checker)
paulson@7144
     7
paulson@7144
     8
Based upon the work of Søren T. Heilmann
paulson@7144
     9
*)
paulson@7144
    10
wenzelm@7237
    11
theory SVC_Oracle = NatBin (** + Real??**)
wenzelm@7237
    12
files "Tools/svc_funcs.ML":
paulson@7162
    13
paulson@7162
    14
consts
paulson@7162
    15
  (*reserved for the oracle*)
wenzelm@7237
    16
  iff_keep :: "[bool, bool] => bool"
wenzelm@7237
    17
  iff_unfold :: "[bool, bool] => bool"
paulson@7162
    18
wenzelm@7237
    19
oracle
wenzelm@7237
    20
  svc_oracle = Svc.oracle
wenzelm@7237
    21
paulson@7144
    22
end