(* 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 *) Buffer_adm = Buffer + Stream_adm