(* Title: HOLCF/FOCUS/FOCUS.thy ID: $ $ Author: David von Oheimb, TU Muenchen License: GPL (GNU GENERAL PUBLIC LICENSE) top level of FOCUS *) FOCUS = Fstream