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
paulson@7144
     1
(*  Title:      HOL/SVC_Oracle
paulson@7144
     2
    ID:         $Id$
paulson@7144
     3
    Author:     Lawrence C Paulson
paulson@7144
     4
    Copyright   1999  University of Cambridge
paulson@7144
     5
paulson@7144
     6
Installing the oracle for SVC (Stanford Validity Checker)
paulson@7144
     7
paulson@7144
     8
Based upon the work of Søren T. Heilmann
paulson@7144
     9
*)
paulson@7144
    10
paulson@7144
    11
SVC_Oracle = NatBin + (**Real?? + **)
paulson@7144
    12
oracle svc_oracle = Svc.oracle
paulson@7144
    13
end