Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/SVC_Oracle.thy
author kleing
Sat, 17 Apr 2004 00:46:22 +0200
changeset 14610 9c2e31e483b2
parent 12869 f362c0323d92
child 16417 9bc16273c2d4
permissions -rw-r--r--
added HOL-Matrix, added HOL/Matrix/ROOT.ML

(*  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
isabelle