src/HOL/SVC_Oracle.thy
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 7237 2919daadba91
permissions -rw-r--r--
tidied; added lemma restrict_to_left
wenzelm@7237
     1
(*  Title:      HOL/SVC_Oracle.thy
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
wenzelm@7237
    11
theory SVC_Oracle = NatBin (** + Real??**)
wenzelm@7237
    12
files "Tools/svc_funcs.ML":
paulson@7162
    13
paulson@7162
    14
consts
paulson@7162
    15
  (*reserved for the oracle*)
wenzelm@7237
    16
  iff_keep :: "[bool, bool] => bool"
wenzelm@7237
    17
  iff_unfold :: "[bool, bool] => bool"
paulson@7162
    18
wenzelm@7237
    19
oracle
wenzelm@7237
    20
  svc_oracle = Svc.oracle
wenzelm@7237
    21
paulson@7144
    22
end