author | wenzelm |
Wed, 14 Sep 2005 22:08:08 +0200 | |
changeset 17388 | 495c799df31d |
parent 16836 | 45a3dc4688bc |
child 20813 | 379ce56e5dc2 |
permissions | -rw-r--r-- |
(* Title: HOL/ex/SVC_Oracle.thy ID: $Id$ Author: Lawrence C Paulson Copyright 1999 University of Cambridge Based upon the work of Søren T. Heilmann. *) header {* Installing an oracle for SVC (Stanford Validity Checker) *} theory SVC_Oracle imports Main uses "svc_funcs.ML" begin consts iff_keep :: "[bool, bool] => bool" iff_unfold :: "[bool, bool] => bool" hide const iff_keep iff_unfold oracle svc_oracle ("term") = Svc.oracle end