isabelle: src/HOL/SVC_Oracle.thy@5e4bba59bfaa (annotated)

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

author	wenzelm
	Mon, 13 Mar 2000 13:21:39 +0100
changeset 8434	5e4bba59bfaa
parent 7237	2919daadba91
permissions	-rw-r--r--