(* Title: HOLCF/FOCUS/FOCUS.thy ID: $Id: FOCUS.thy,v 1.4 2005/09/06 19:51:17 wenzelm Exp $ Author: David von Oheimb, TU Muenchen *) header {* Top level of FOCUS *} theory FOCUS imports Fstream begin end
theorem fstream_exhaust_slen_eq:
(#x ≠ 0) = (∃a y. x = a~>y)