src/HOLCF/FOCUS/Stream_adm.thy
2010-11-27 huffman 2010-11-27 renamed several HOLCF theorems (listed in NEWS)
2010-11-03 huffman 2010-11-03 discontinue a bunch of legacy theorem names
2010-11-03 huffman 2010-11-03 move a few admissibility lemmas into FOCUS/Stream_adm.thy
2010-05-24 huffman 2010-05-24 move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
2010-02-17 huffman 2010-02-17 remove $ from all HOLCF files
2009-05-10 nipkow 2009-05-10 fixed HOLCF proofs
2008-07-01 huffman 2008-07-01 replace lub (range Y) with (LUB i. Y i)
2008-06-10 haftmann 2008-06-10 slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
2008-05-07 berghofe 2008-05-07 Instantiated rule increasing_chain_adm_lemma in proof of flatstream_adm_lemma to avoid problems with HO unification.
2008-03-27 wenzelm 2008-03-27 avoid amiguity of Continuity.chain vs. Porder.chain;
2008-02-20 huffman 2008-02-20 fix proofs involving ile_def
2007-07-31 wenzelm 2007-07-31 proper path specifications;
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-06-02 wenzelm 2006-06-02 tuned;
2006-06-01 huffman 2006-06-01 removed legacy ML scripts
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;
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2001-10-03 wenzelm 2001-10-03 tuned parentheses in relational expressions;
2001-05-31 wenzelm 2001-05-31 tuned
2001-05-31 oheimb 2001-05-31 added FOCUS including the One-Element Buffer by Manfred Broy