| author | nipkow |
| Wed, 18 Aug 2004 11:09:40 +0200 | |
| changeset 15140 | 322485b816ac |
| parent 12869 | f362c0323d92 |
| child 16417 | 9bc16273c2d4 |
| permissions | -rw-r--r-- |
| 12869 | 1 |
(* Title: HOL/ex/SVC_Oracle.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson |
|
4 |
Copyright 1999 University of Cambridge |
|
5 |
||
6 |
Installing the oracle for SVC (Stanford Validity Checker) |
|
7 |
||
8 |
Based upon the work of Søren T. Heilmann |
|
9 |
*) |
|
10 |
||
11 |
theory SVC_Oracle = Main (** + Real??**) |
|
12 |
files "svc_funcs.ML": |
|
13 |
||
14 |
consts |
|
15 |
(*reserved for the oracle*) |
|
16 |
iff_keep :: "[bool, bool] => bool" |
|
17 |
iff_unfold :: "[bool, bool] => bool" |
|
18 |
||
19 |
oracle |
|
20 |
svc_oracle = Svc.oracle |
|
21 |
||
22 |
end |