src/HOL/SVC_Oracle.thy
author paulson
Mon Aug 02 11:26:43 1999 +0200 (1999-08-02)
changeset 7144 0feee8201d67
child 7162 8737390d1d0a
permissions -rw-r--r--
the SVC oracle theory
     1 (*  Title:      HOL/SVC_Oracle
     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 SVC_Oracle = NatBin + (**Real?? + **)
    12 oracle svc_oracle = Svc.oracle
    13 end