src/HOLCF/ex/Stream.thy
2007-04-26 wenzelm 2007-04-26 eliminated unnamed infixes, tuned syntax;
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-06-02 wenzelm 2006-06-02 tuned;
2006-05-03 huffman 2006-05-03 update to reflect changes in inverts/injects lemmas
2006-04-13 huffman 2006-04-13 add lemma less_UU_iff as default simp rule
2005-11-07 wenzelm 2005-11-07 avoid 'as' as identifier;
2005-11-03 huffman 2005-11-03 changed iterate to a continuous type
2005-09-06 wenzelm 2005-09-06 converted to Isar theory format;
2005-07-07 huffman 2005-07-07 fixes to work with UU_reorient_simproc
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-06-03 huffman 2005-06-03 fixed some renamed theorems
2004-09-07 oheimb 2004-09-07 integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-04-12 oheimb 2004-04-12 added Streams.thy (with stream concatenation etc.)
2003-08-28 skalberg 2003-08-28 Extended the notion of letter and digit, such that now one may use greek, gothic, euler, or calligraphic letters as normal letters.
2001-11-03 wenzelm 2001-11-03 GPLed;
2001-05-31 oheimb 2001-05-31 added stream length, map, and filter
2000-06-28 paulson 2000-06-28 tidying and unbatchifying
1997-11-04 oheimb 1997-11-04 * removed "axioms" and "generated by" section * replaced "ops" section by extended "consts" section, which is capable of handling the continuous function space "->" directly * domain package: now uses normal mixfix annotations (instead of cinfix...)
1997-01-31 oheimb 1997-01-31 added Classlib.* and Witness.*, moved (and updated) Coind.*, Dagstuhl.*, Dlist.*, Dnat.*, Focus_ex.* and Stream.* from HOLCF/explicit_domains to here adapted several proofs; now they work again. Hope that the following strange errors (when committing) do not matter: rlog error: RCS/Classlib.ML,v: No such file or directory rlog error: RCS/Classlib.thy,v: No such file or directory rlog error: RCS/Coind.ML,v: No such file or directory rlog error: RCS/Coind.thy,v: No such file or directory rlog error: RCS/Dagstuhl.ML,v: No such file or directory rlog error: RCS/Dagstuhl.thy,v: No such file or directory rlog error: RCS/Dlist.ML,v: No such file or directory rlog error: RCS/Dlist.thy,v: No such file or directory rlog error: RCS/Dnat.ML,v: No such file or directory rlog error: RCS/Dnat.thy,v: No such file or directory rlog error: RCS/Focus_ex.ML,v: No such file or directory rlog error: RCS/Focus_ex.thy,v: No such file or directory rlog error: RCS/Stream.ML,v: No such file or directory rlog error: RCS/Stream.thy,v: No such file or directory rlog error: RCS/Witness.ML,v: No such file or directory rlog error: RCS/Witness.thy,v: No such file or directory