Up to index of Isabelle/HOL/ex
theory SVC_Oracle(* Title: HOL/ex/SVC_Oracle.thy ID: $Id: SVC_Oracle.thy,v 1.4 2005/09/14 20:08:09 wenzelm Exp $ 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