Old_HOL: IOA/example/Correctness.thy@492493334e0f (annotated)

168 44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	1	(* Title: HOL/IOA/example/Correctness.thy
44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	2	ID: $Id$
44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	3	Author: Tobias Nipkow & Konrad Slind
44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	4	Copyright 1994 TU Muenchen
44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	5
44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	6	The main correctness proof: Impl implements Spec
44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	7	*)
44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	8
44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	9	Correctness = Solve + Impl + Spec +
156 fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	10
fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	11	consts
fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	12
fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	13	hom :: "'m impl_state => 'm list"
fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	14
168 44ff2275d44f Added headers and made various small mods. nipkow parents: 156 diff changeset	15	defs
156 fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	16
fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	17	hom_def
249 492493334e0f removed \...\ inside strings clasohm parents: 168 diff changeset	18	"hom(s) == rq(rec(s)) @ if(rbit(rec(s)) = sbit(sen(s)),
492493334e0f removed \...\ inside strings clasohm parents: 168 diff changeset	19	sq(sen(s)),
492493334e0f removed \...\ inside strings clasohm parents: 168 diff changeset	20	ttl(sq(sen(s))))"
156 fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	21
fd1be45b64bf added IOA to isabelle/HOL clasohm parents: diff changeset	22	end

author	clasohm
	Wed, 21 Jun 1995 15:12:40 +0200
changeset 249	492493334e0f
parent 168	44ff2275d44f
permissions	-rw-r--r--