isabelle: src/HOL/ex/SVC_Oracle.thy@c1ce129e6f9c (annotated)

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
17388 495c799df31d tuned headers etc.; wenzelm parents: 16836 diff changeset	6	Based upon the work of S�ren T. Heilmann.
495c799df31d tuned headers etc.; wenzelm parents: 16836 diff changeset	7	*)
12869 f362c0323d92 moved SVC stuff to ex; wenzelm parents: diff changeset	8
17388 495c799df31d tuned headers etc.; wenzelm parents: 16836 diff changeset	9	header {* Installing an oracle for SVC (Stanford Validity Checker) *}
12869 f362c0323d92 moved SVC stuff to ex; wenzelm parents: diff changeset	10
16836 45a3dc4688bc improved oracle setup; wenzelm parents: 16417 diff changeset	11	theory SVC_Oracle
45a3dc4688bc improved oracle setup; wenzelm parents: 16417 diff changeset	12	imports Main
20813 379ce56e5dc2 proper use of svc_oracle.ML; wenzelm parents: 17388 diff changeset	13	uses "svc_funcs.ML" ("svc_oracle.ML")
16836 45a3dc4688bc improved oracle setup; wenzelm parents: 16417 diff changeset	14	begin
12869 f362c0323d92 moved SVC stuff to ex; wenzelm parents: diff changeset	15
f362c0323d92 moved SVC stuff to ex; wenzelm parents: diff changeset	16	consts
f362c0323d92 moved SVC stuff to ex; wenzelm parents: diff changeset	17	iff_keep :: "[bool, bool] => bool"
f362c0323d92 moved SVC stuff to ex; wenzelm parents: diff changeset	18	iff_unfold :: "[bool, bool] => bool"
f362c0323d92 moved SVC stuff to ex; wenzelm parents: diff changeset	19
16836 45a3dc4688bc improved oracle setup; wenzelm parents: 16417 diff changeset	20	hide const iff_keep iff_unfold
45a3dc4688bc improved oracle setup; wenzelm parents: 16417 diff changeset	21
12869 f362c0323d92 moved SVC stuff to ex; wenzelm parents: diff changeset	22	oracle
16836 45a3dc4688bc improved oracle setup; wenzelm parents: 16417 diff changeset	23	svc_oracle ("term") = Svc.oracle
12869 f362c0323d92 moved SVC stuff to ex; wenzelm parents: diff changeset	24
20813 379ce56e5dc2 proper use of svc_oracle.ML; wenzelm parents: 17388 diff changeset	25	use "svc_oracle.ML"
379ce56e5dc2 proper use of svc_oracle.ML; wenzelm parents: 17388 diff changeset	26
12869 f362c0323d92 moved SVC stuff to ex; wenzelm parents: diff changeset	27	end

author	krauss
	Thu, 17 May 2007 22:33:41 +0200
changeset 22999	c1ce129e6f9c
parent 20813	379ce56e5dc2
child 24470	41c81e23c08d
permissions	-rw-r--r--