src/HOL/ex/SVC_Oracle.thy
author haftmann
Fri, 17 Jun 2005 16:12:49 +0200
changeset 16417 9bc16273c2d4
parent 12869 f362c0323d92
child 16836 45a3dc4688bc
permissions -rw-r--r--
migrated theory headers to new format
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12869
f362c0323d92 moved SVC stuff to ex;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/ex/SVC_Oracle.thy
f362c0323d92 moved SVC stuff to ex;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
f362c0323d92 moved SVC stuff to ex;
wenzelm
parents:
diff changeset
     3
    Author:     Lawrence C Paulson
f362c0323d92 moved SVC stuff to ex;
wenzelm
parents:
diff changeset
     4
    Copyright   1999  University of Cambridge
f362c0323d92 moved SVC stuff to ex;
wenzelm
parents:
diff changeset
     5
f362c0323d92 moved SVC stuff to ex;
wenzelm
parents:
diff changeset
     6
Installing the oracle for SVC (Stanford Validity Checker)
f362c0323d92 moved SVC stuff to ex;
wenzelm
parents:
diff changeset
     7
f362c0323d92 moved SVC stuff to ex;
wenzelm
parents:
diff changeset
     8
Based upon the work of Søren T. Heilmann
f362c0323d92 moved SVC stuff to ex;
wenzelm
parents:
diff changeset
     9
*)
f362c0323d92 moved SVC stuff to ex;
wenzelm
parents:
diff changeset
    10
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 12869
diff changeset
    11
theory SVC_Oracle imports Main (** + Real??**)
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 12869
diff changeset
    12
uses "svc_funcs.ML" begin
12869
f362c0323d92 moved SVC stuff to ex;
wenzelm
parents:
diff changeset
    13
f362c0323d92 moved SVC stuff to ex;
wenzelm
parents:
diff changeset
    14
consts
f362c0323d92 moved SVC stuff to ex;
wenzelm
parents:
diff changeset
    15
  (*reserved for the oracle*)
f362c0323d92 moved SVC stuff to ex;
wenzelm
parents:
diff changeset
    16
  iff_keep :: "[bool, bool] => bool"
f362c0323d92 moved SVC stuff to ex;
wenzelm
parents:
diff changeset
    17
  iff_unfold :: "[bool, bool] => bool"
f362c0323d92 moved SVC stuff to ex;
wenzelm
parents:
diff changeset
    18
f362c0323d92 moved SVC stuff to ex;
wenzelm
parents:
diff changeset
    19
oracle
f362c0323d92 moved SVC stuff to ex;
wenzelm
parents:
diff changeset
    20
  svc_oracle = Svc.oracle
f362c0323d92 moved SVC stuff to ex;
wenzelm
parents:
diff changeset
    21
f362c0323d92 moved SVC stuff to ex;
wenzelm
parents:
diff changeset
    22
end