(* Title: HOLCF/FOCUS/Buffer_adm.thy ID: $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