src/HOLCF/ex/Hoare.thy
2010-10-16 huffman 2010-10-16 remove old uses of 'simp_tac HOLCF_ss'
2010-10-11 huffman 2010-10-11 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
2010-03-24 huffman 2010-03-24 remove ancient continuity tactic
2010-02-17 huffman 2010-02-17 remove $ from all HOLCF files
2008-05-17 wenzelm 2008-05-17 avoid undeclared variables in facts;
2008-03-19 wenzelm 2008-03-19 removed redundant Nat.less_irrefl;
2008-01-14 huffman 2008-01-14 converted adm_all and adm_ball to rule_format; cleaned up
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;
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2001-11-03 wenzelm 2001-11-03 GPLed;
2001-01-09 nipkow 2001-01-09 ` -> $
1996-12-13 sandnerr 1996-12-13 Dummy change to document the change in revision 1.5: Parent theory changed to HOLCF.thy (former Tr2.thy) . Was necessary because the use of HOLCF_ss in Hoare.ML, which has been extended by the introduction of the Lift theories.
1996-12-13 sandnerr 1996-12-13 ex/Hoare.thy
1996-02-06 clasohm 1996-02-06 expanded tabs
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-06-21 clasohm 1995-06-21 removed \...\ inside strings
1994-01-19 nipkow 1994-01-19 HOLCF examples