isabelle: src/HOLCF/FOCUS/Buffer_adm.thy@3414c04fbc39 (annotated)

17293 ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	1	(* Title: HOLCF/FOCUS/Buffer_adm.thy
11355 778c369559d9 tuned wenzelm parents: 11350 diff changeset	2	ID: $Id$
17293 ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	3	Author: David von Oheimb, TU Muenchen
11350 4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	4	*)
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	5
17293 ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	6	header {* One-element buffer, proof of Buf_Eq_imp_AC by induction + admissibility *}
11350 4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	7
17293 ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	8	theory Buffer_adm
ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	imports Buffer Stream_adm
ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	10	begin
ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	11
ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	12	end
ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	13
ecf182ccc3ca converted to Isar theory format; wenzelm parents: 14981 diff changeset	14

author	haftmann
	Thu, 06 Apr 2006 16:08:25 +0200
changeset 19341	3414c04fbc39
parent 17293	ecf182ccc3ca
child 19759	2d0896653e7a
permissions	-rw-r--r--