|
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 |
|
|
16836
|
11 |
theory SVC_Oracle
|
|
|
12 |
imports Main
|
|
|
13 |
uses "svc_funcs.ML"
|
|
|
14 |
begin
|
|
12869
|
15 |
|
|
|
16 |
consts
|
|
|
17 |
iff_keep :: "[bool, bool] => bool"
|
|
|
18 |
iff_unfold :: "[bool, bool] => bool"
|
|
|
19 |
|
|
16836
|
20 |
hide const iff_keep iff_unfold
|
|
|
21 |
|
|
12869
|
22 |
oracle
|
|
16836
|
23 |
svc_oracle ("term") = Svc.oracle
|
|
12869
|
24 |
|
|
|
25 |
end
|