--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/FOCUS/Buffer_adm.thy	Thu May 31 16:53:00 2001 +0200
@@ -0,0 +1,10 @@
+(*  Title: 	HOLCF/FOCUS/Buffer_adm.thy
+    ID:         $ $
+    Author: 	David von Oheimb, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+
+One-element buffer, proof of Buf_Eq_imp_AC by induction + admissibility
+*)
+
+Buffer_adm = Buffer + Stream_adm
+