src/HOL/SVC_Oracle.thy
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 7237 2919daadba91
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.

(*  Title:      HOL/SVC_Oracle.thy
    ID:         $Id$
    Author:     Lawrence C Paulson
    Copyright   1999  University of Cambridge

Installing the oracle for SVC (Stanford Validity Checker)

Based upon the work of Søren T. Heilmann
*)

theory SVC_Oracle = NatBin (** + Real??**)
files "Tools/svc_funcs.ML":

consts
  (*reserved for the oracle*)
  iff_keep :: "[bool, bool] => bool"
  iff_unfold :: "[bool, bool] => bool"

oracle
  svc_oracle = Svc.oracle

end