isabelle: src/HOLCF/IOA/NTP/Correctness.thy@3e47692e3a3e (annotated)

3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	1	(* Title: HOL/IOA/NTP/Correctness.thy
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	2	ID: $Id$
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	3	Author: Tobias Nipkow & Konrad Slind
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	4	Copyright 1994 TU Muenchen
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	5
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	6	The main correctness proof: Impl implements Spec
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	7	*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	8
4816 64f075872f69 simplification of explicit theory usage and merges oheimb parents: 3898 diff changeset	9	Correctness = Impl + Spec +
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	10
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	11	constdefs
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	12
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	13	hom :: 'm impl_state => 'm list
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	14	"hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
3898 f6bf42312e9e Simplified proof. nipkow parents: 3073 diff changeset	15	else tl(sq(sen s)))"
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	16
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	17	end

author	wenzelm
	Thu, 15 Feb 2001 17:18:54 +0100
changeset 11145	3e47692e3a3e
parent 4816	64f075872f69
child 12218	6597093b77e7
permissions	-rw-r--r--