isabelle: src/HOL/IOA/ABP/Packet.thy@0140ff702b23 (annotated)

1050 0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	1	(* Title: HOL/IOA/ABP/Packet.thy
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	2	ID: $Id$
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	3	Author: Tobias Nipkow & Olaf Mueller
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	4	Copyright 1995 TU Muenchen
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
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	15	consts
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	16
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	17	hdr :: "'msg packet => bool"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	18	msg :: "'msg packet => 'msg"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	19
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	20	defs
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	21
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	22	hdr_def "hdr == fst"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	23	msg_def "msg == snd"
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	24
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	25	end

author	lcp
	Tue, 25 Apr 1995 11:14:03 +0200
changeset 1072	0140ff702b23
parent 1050	0c36c6a52a1d
child 1139	993e475e70e2
permissions	-rw-r--r--