isabelle: src/HOL/IOA/ABP/Packet.thy@9741c4c6b62b (annotated)

1139 993e475e70e2 * empty log message * mueller parents: 1050 diff changeset	1	(* Title: HOL/IOA/example/Packet.thy
1050 0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	2	ID: $Id$
1139 993e475e70e2 * empty log message * mueller parents: 1050 diff changeset	3	Author: Tobias Nipkow & Konrad Slind
993e475e70e2 * empty log message * mueller parents: 1050 diff changeset	4	Copyright 1994 TU Muenchen
1050 0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	5
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	6	Packets
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	7	*)
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	8
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	9	Packet = Arith +
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	10
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	11	types
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	12
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	13	'msg packet = "bool * 'msg"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	14
1570 fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	15	constdefs
1050 0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	16
1376 92f83b9d17e1 removed quotes from consts and syntax sections clasohm parents: 1139 diff changeset	17	hdr :: 'msg packet => bool
1570 fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	18	"hdr == fst"
1050 0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	19
1570 fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	20	msg :: 'msg packet => 'msg
fd1b9c721ac7 added constdefs section clasohm parents: 1376 diff changeset	21	"msg == snd"
1050 0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	22
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	23	end

author	nipkow
	Tue, 18 Mar 1997 08:42:18 +0100
changeset 2800	9741c4c6b62b
parent 1570	fd1b9c721ac7
permissions	-rw-r--r--