src/HOLCF/ex/Focus_ex.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-09-06 wenzelm 2010-09-06 more antiquotations;
2010-06-28 haftmann 2010-06-28 explicit is better than implicit
2010-03-22 huffman 2010-03-22 use Pair, fst, snd instead of cpair, cfst, csnd
2010-02-17 huffman 2010-02-17 remove $ from all HOLCF files
2008-06-12 huffman 2008-06-12 change orientation of fix_eqI and convert to rule_format; add lemma fix_ind2
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-10-10 wenzelm 1997-10-10 fixed dots;
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