src/HOL/SVC_Oracle.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 7237 2919daadba91
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7237
2919daadba91 turned SVC_Oracle into a new-style theory in order to get automatic
wenzelm
parents: 7162
diff changeset
     1
(*  Title:      HOL/SVC_Oracle.thy
7144
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
     2
    ID:         $Id$
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
     4
    Copyright   1999  University of Cambridge
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
     5
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
     6
Installing the oracle for SVC (Stanford Validity Checker)
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
     7
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
     8
Based upon the work of Søren T. Heilmann
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
     9
*)
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
    10
7237
2919daadba91 turned SVC_Oracle into a new-style theory in order to get automatic
wenzelm
parents: 7162
diff changeset
    11
theory SVC_Oracle = NatBin (** + Real??**)
2919daadba91 turned SVC_Oracle into a new-style theory in order to get automatic
wenzelm
parents: 7162
diff changeset
    12
files "Tools/svc_funcs.ML":
7162
8737390d1d0a biconditionals and the natural numbers
paulson
parents: 7144
diff changeset
    13
8737390d1d0a biconditionals and the natural numbers
paulson
parents: 7144
diff changeset
    14
consts
8737390d1d0a biconditionals and the natural numbers
paulson
parents: 7144
diff changeset
    15
  (*reserved for the oracle*)
7237
2919daadba91 turned SVC_Oracle into a new-style theory in order to get automatic
wenzelm
parents: 7162
diff changeset
    16
  iff_keep :: "[bool, bool] => bool"
2919daadba91 turned SVC_Oracle into a new-style theory in order to get automatic
wenzelm
parents: 7162
diff changeset
    17
  iff_unfold :: "[bool, bool] => bool"
7162
8737390d1d0a biconditionals and the natural numbers
paulson
parents: 7144
diff changeset
    18
7237
2919daadba91 turned SVC_Oracle into a new-style theory in order to get automatic
wenzelm
parents: 7162
diff changeset
    19
oracle
2919daadba91 turned SVC_Oracle into a new-style theory in order to get automatic
wenzelm
parents: 7162
diff changeset
    20
  svc_oracle = Svc.oracle
2919daadba91 turned SVC_Oracle into a new-style theory in order to get automatic
wenzelm
parents: 7162
diff changeset
    21
7144
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
    22
end