src/HOLCF/ex/Dagstuhl.thy
2010-03-07 huffman 2010-03-07 generate separate qualified theorem name for each type's reach and take_lemma
2010-02-17 huffman 2010-02-17 remove $ from all HOLCF files
2010-02-17 huffman 2010-02-17 fix warnings about duplicate simp rules
2007-10-21 wenzelm 2007-10-21 modernized specifications ('definition', 'axiomatization');
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-06-02 wenzelm 2006-06-02 tuned;
2006-05-28 wenzelm 2006-05-28 removed legacy ML scripts;
2005-09-06 wenzelm 2005-09-06 converted to Isar theory format;
2001-01-09 nipkow 2001-01-09 ` -> $
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
1995-06-29 regensbu 1995-06-29 The curried version of HOLCF is now just called HOLCF. The old uncurried version is no longer supported
1995-02-07 regensbu 1995-02-07 ID for the file
1994-03-24 nipkow 1994-03-24 Franz fragen