src/HOL/SVC_Oracle.thy
changeset 7144 0feee8201d67
child 7162 8737390d1d0a
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SVC_Oracle.thy	Mon Aug 02 11:26:43 1999 +0200
     1.3 @@ -0,0 +1,13 @@
     1.4 +(*  Title:      HOL/SVC_Oracle
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson
     1.7 +    Copyright   1999  University of Cambridge
     1.8 +
     1.9 +Installing the oracle for SVC (Stanford Validity Checker)
    1.10 +
    1.11 +Based upon the work of Søren T. Heilmann
    1.12 +*)
    1.13 +
    1.14 +SVC_Oracle = NatBin + (**Real?? + **)
    1.15 +oracle svc_oracle = Svc.oracle
    1.16 +end