--- a/src/HOLCF/FOCUS/Buffer_adm.thy Tue Sep 06 20:53:27 2005 +0200
+++ b/src/HOLCF/FOCUS/Buffer_adm.thy Tue Sep 06 21:51:17 2005 +0200
@@ -1,9 +1,14 @@
-(* Title: HOLCF/FOCUS/Buffer_adm.thy
+(* Title: HOLCF/FOCUS/Buffer_adm.thy
ID: $Id$
- Author: David von Oheimb, TU Muenchen
-
-One-element buffer, proof of Buf_Eq_imp_AC by induction + admissibility
+ Author: David von Oheimb, TU Muenchen
*)
-Buffer_adm = Buffer + Stream_adm
+header {* One-element buffer, proof of Buf_Eq_imp_AC by induction + admissibility *}
+theory Buffer_adm
+imports Buffer Stream_adm
+begin
+
+end
+
+