src/HOLCF/Cont.thy
2010-03-22 huffman 2010-03-22 remove LaTeX hyperref warnings by avoiding antiquotations within section headings
2010-03-14 huffman 2010-03-14 use headers consistently
2009-07-02 wenzelm 2009-07-02 renamed NamedThmsFun to Named_Thms; simplified/unified names of instances of Named_Thms;
2009-05-08 huffman 2009-05-08 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
2009-05-06 huffman 2009-05-06 replace cont2cont_apply with cont_apply; add new cont2cont lemmas
2009-04-30 huffman 2009-04-30 use simproc_setup command for cont_proc
2009-01-15 huffman 2009-01-15 use match_tac instead of resolve_tac for continuity simproc
2009-01-14 huffman 2009-01-14 add lemmas cont2monofunE, cont2cont_apply
2009-01-14 huffman 2009-01-14 change to simpler, more extensible continuity simproc define attribute [cont2cont] for continuity rules; new continuity simproc just applies cont2cont rules repeatedly; split theory Product_Cpo from Cprod, so Cfun can import Product_Cpo; add lemma cont2cont_LAM', which is suitable as a cont2cont rule.
2008-12-16 huffman 2008-12-16 remove cvs Id tags
2008-07-01 huffman 2008-07-01 remove unused lemmas ub2ub_monofun' and dir2dir_monofun
2008-07-01 huffman 2008-07-01 replace lub (range Y) with (LUB i. Y i)
2008-03-27 huffman 2008-03-27 declare cont_lemmas_ext as simp rules individually
2008-01-31 huffman 2008-01-31 add lemma cpo_lubI
2008-01-31 huffman 2008-01-31 new lemma cont_discrete_cpo
2008-01-16 huffman 2008-01-16 change class axiom ax_flat to rule_format
2008-01-14 huffman 2008-01-14 add lemma contI2
2008-01-03 huffman 2008-01-03 generalized chfindom_monofun2cont
2008-01-02 huffman 2008-01-02 move lemmas from Cont.thy to Ffun.thy; reorder dependency of Cont.thy and Ffun.thy; add dcpo instance proofs for function type
2008-01-02 huffman 2008-01-02 add lemma ub2ub_monofun'
2008-01-02 huffman 2008-01-02 add lemma dir2dir_monofun
2007-10-21 wenzelm 2007-10-21 modernized specifications ('definition', 'abbreviation', 'notation');
2005-11-05 huffman 2005-11-05 renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
2005-11-04 huffman 2005-11-04 cleaned up
2005-10-11 huffman 2005-10-11 cleaned up; renamed less_fun to expand_fun_less
2005-07-07 huffman 2005-07-07 add lemmas ch2ch_cont and cont2contlubE
2005-07-01 huffman 2005-07-01 cleaned up; reorganized and added section headings
2005-06-25 huffman 2005-06-25 cleaned up proof of contlub_abstraction
2005-06-14 huffman 2005-06-14 renamed theorem cont2cont_CF1L_rev2 to cont2cont_lambda
2005-06-03 huffman 2005-06-03 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
2005-05-27 huffman 2005-05-27 added lemmas monofun_lub_fun and cont_lub_fun
2005-05-25 wenzelm 2005-05-25 removed LICENCE note -- everything is subject to Isabelle licence as stated in COPYRIGHT file;
2005-05-23 huffman 2005-05-23 moved theorem cont2cont_CF1L_rev2 to Cont.thy
2005-03-10 huffman 2005-03-10 fixed filename in header
2005-03-08 huffman 2005-03-08 arranged for document generation, cleaned up some proofs
2005-03-04 huffman 2005-03-04 fix headers
2005-03-04 huffman 2005-03-04 converted to new-style theories, and combined numbered files
2005-03-02 huffman 2005-03-02 converted to new-style theory
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2001-11-03 wenzelm 2001-11-03 GPLed;
1998-03-10 oheimb 1998-03-10 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-05-25 slotosch 1997-05-25 eliminated the constant less by the introduction of the axclass sq_ord added explicit type ::'a::po in the following theorems: minimal2UU,antisym_less_inverse,box_less,not_less2not_eq,monofun_pair and dist_eqI (in domain-package) added instances instance fun :: (term,sq_ord)sq_ord instance "->" :: (term,sq_ord)sq_ord instance "**" :: (sq_ord,sq_ord)sq_ord instance "*" :: (sq_ord,sq_ord)sq_ord instance "++" :: (pcpo,pcpo)sq_ord instance u :: (sq_ord)sq_ord instance lift :: (term)sq_ord instance discr :: (term)sq_ord
1997-03-25 slotosch 1997-03-25 changed continuous functions from pcpo to cpo (including instances)
1996-02-06 clasohm 1996-02-06 expanded tabs
1995-10-06 regensbu 1995-10-06 added 8bit pragmas added directory ax_ops for sections axioms and ops added directory domain for sections domain and generated this is the type definition package of David Oheimb
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 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF in HOL.