isabelle: src/HOL/IOA/NTP/Correctness.thy@5a5e508e2a2b (annotated)

1051 4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	1	(* Title: HOL/IOA/NTP/Correctness.thy
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	2	ID: $Id$
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	3	Author: Tobias Nipkow & Konrad Slind
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	4	Copyright 1994 TU Muenchen
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	5
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	6	The main correctness proof: Impl implements Spec
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	7	*)
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	8
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	9	Correctness = Solve + Impl + Spec +
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	10
1570 fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	11	constdefs
1051 4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	12
1570 fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	13	hom :: 'm impl_state => 'm list
fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	14	"hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	15	else ttl(sq(sen s)))"
1051 4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	16
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	17	end

author	paulson
	Mon, 07 Oct 1996 10:55:51 +0200
changeset 2064	5a5e508e2a2b
parent 1570	fd1b9c721ac7
permissions	-rw-r--r--