added FOCUS including the One-Element Buffer by Manfred Broy
(* 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