src/HOLCF/Cprod.thy
2010-03-22 huffman 2010-03-22 completely remove constants cpair, cfst, csnd
2010-03-22 huffman 2010-03-22 define csplit using fst, snd
2010-03-22 huffman 2010-03-22 remove LaTeX hyperref warnings by avoiding antiquotations within section headings
2009-11-02 huffman 2009-11-02 add (LAM (x, y). t) syntax and lemma csplit_Pair
2009-05-11 huffman 2009-05-11 move bifinite instance for product type from Cprod.thy to Bifinite.thy
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-01-15 huffman 2009-01-15 add strictness and compactness lemmas to Product_Cpo.thy
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 replace lub (range Y) with (LUB i. Y i)
2008-06-20 huffman 2008-06-20 simplify profinite class axioms
2008-05-19 huffman 2008-05-19 use new class package for classes profinite, bifinite; remove approx class
2008-03-26 huffman 2008-03-26 rename class bifinite_cpo to profinite; generalize powerdomains from bifinite to profinite
2008-02-02 huffman 2008-02-02 instance "*" :: (sq_ord, sq_ord) sq_ord
2008-02-01 huffman 2008-02-01 add lemmas prod_lessI and Pair_less_iff [simp]
2008-01-31 huffman 2008-01-31 add lemma cpo_lubI
2008-01-31 huffman 2008-01-31 instances for class discrete_cpo
2008-01-31 huffman 2008-01-31 new lemma is_lub_Pair; cleaned up some proofs
2008-01-17 huffman 2008-01-17 change class axiom chfin to rule_format
2008-01-15 huffman 2008-01-15 declare cpair_strict [simp]
2008-01-14 huffman 2008-01-14 add bifinite instances
2008-01-14 huffman 2008-01-14 cleaned up instance proofs
2008-01-14 huffman 2008-01-14 new-style instantiation proof for unit :: po
2008-01-14 huffman 2008-01-14 class bifinite supersedes class dcpo; remove unnecessary dcpo stuff
2008-01-14 huffman 2008-01-14 simplified chfin instance proof
2008-01-10 huffman 2008-01-10 new compactness lemmas
2008-01-04 huffman 2008-01-04 new instance proofs for classes finite_po, chfin, flat
2008-01-03 huffman 2008-01-03 instance unit :: finite_po
2008-01-02 huffman 2008-01-02 update instance proofs for sq_ord, po; new instance proofs for dcpo
2007-10-21 wenzelm 2007-10-21 modernized specifications ('definition', 'abbreviation', 'notation');
2005-11-30 huffman 2005-11-30 add constant unit_when
2005-11-03 huffman 2005-11-03 change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
2005-11-03 huffman 2005-11-03 make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
2005-10-12 huffman 2005-10-12 added compactness lemmas; cleaned up
2005-10-11 huffman 2005-10-11 added xsymbols syntax for pairs; cleaned up
2005-10-10 huffman 2005-10-10 new syntax translations for continuous lambda abstraction
2005-07-26 huffman 2005-07-26 add theorem cpair_defined_iff
2005-07-08 huffman 2005-07-08 add lemma eq_cprod
2005-06-23 huffman 2005-06-23 add csplit3, ssplit3, fup3 as simp rules
2005-06-08 huffman 2005-06-08 added theorem less_cprod
2005-06-03 huffman 2005-06-03 changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
2005-05-27 huffman 2005-05-27 use thelub_const lemma
2005-05-26 huffman 2005-05-26 cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
2005-05-25 wenzelm 2005-05-25 removed LICENCE note -- everything is subject to Isabelle licence as stated in COPYRIGHT file;
2005-05-24 huffman 2005-05-24 added lemma cpair_eq, made cfst_strict and csnd_strict into simp rules
2005-05-19 huffman 2005-05-19 pcpo instance for type unit
2005-03-14 huffman 2005-03-14 fixed syntax for Let <x,y> = a in e
2005-03-10 huffman 2005-03-10 fixed filename in header
2005-03-08 huffman 2005-03-08 reordered and 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