author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 7237  2919daadba91 
permissions  rwrr 
7237
2919daadba91
turned SVC_Oracle into a newstyle theory in order to get automatic
wenzelm
parents:
7162
diff
changeset

1 
(* Title: HOL/SVC_Oracle.thy 
7144  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 

7237
2919daadba91
turned SVC_Oracle into a newstyle theory in order to get automatic
wenzelm
parents:
7162
diff
changeset

11 
theory SVC_Oracle = NatBin (** + Real??**) 
2919daadba91
turned SVC_Oracle into a newstyle theory in order to get automatic
wenzelm
parents:
7162
diff
changeset

12 
files "Tools/svc_funcs.ML": 
7162  13 

14 
consts 

15 
(*reserved for the oracle*) 

7237
2919daadba91
turned SVC_Oracle into a newstyle theory in order to get automatic
wenzelm
parents:
7162
diff
changeset

16 
iff_keep :: "[bool, bool] => bool" 
2919daadba91
turned SVC_Oracle into a newstyle theory in order to get automatic
wenzelm
parents:
7162
diff
changeset

17 
iff_unfold :: "[bool, bool] => bool" 
7162  18 

7237
2919daadba91
turned SVC_Oracle into a newstyle theory in order to get automatic
wenzelm
parents:
7162
diff
changeset

19 
oracle 
2919daadba91
turned SVC_Oracle into a newstyle theory in order to get automatic
wenzelm
parents:
7162
diff
changeset

20 
svc_oracle = Svc.oracle 
2919daadba91
turned SVC_Oracle into a newstyle theory in order to get automatic
wenzelm
parents:
7162
diff
changeset

21 

7144  22 
end 