author | kleing |
Sat, 01 Mar 2003 16:45:51 +0100 | |
changeset 13840 | 399c8103a98f |
parent 12869 | f362c0323d92 |
child 16417 | 9bc16273c2d4 |
permissions | -rw-r--r-- |
(* Title: HOL/ex/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 = Main (** + Real??**) files "svc_funcs.ML": consts (*reserved for the oracle*) iff_keep :: "[bool, bool] => bool" iff_unfold :: "[bool, bool] => bool" oracle svc_oracle = Svc.oracle end