src/HOLCF/Ssum.thy
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-10-09 huffman 2010-10-09 move all bifinite class instances to Bifinite.thy
2010-10-08 huffman 2010-10-08 rename class 'sfp' to 'bifinite'
2010-10-06 huffman 2010-10-06 major reorganization/simplification of HOLCF type classes: removed profinite/bifinite classes and approx function; universal domain uses approx_chain locale instead of bifinite class; ideal_completion locale does not use 'take' functions, requires countable basis instead; replaced type 'udom alg_defl' with type 'sfp'; replaced class 'rep' with class 'sfp'; renamed REP('a) to SFP('a);
2010-10-05 Brian Huffman 2010-10-05 add lemma finite_deflation_intro
2010-04-28 wenzelm 2010-04-28 renamed command 'defaultsort' to 'default_sort';
2010-03-22 huffman 2010-03-22 remove LaTeX hyperref warnings by avoiding antiquotations within section headings
2010-03-13 huffman 2010-03-13 declare case_names for various induction rules
2010-03-03 wenzelm 2010-03-03 merged, resolving some basic conflicts;
2010-03-02 huffman 2010-03-02 proper names for types cfun, sprod, ssum
2010-03-01 huffman 2010-03-01 add lemmas about ssum_map and sprod_map
2010-03-02 wenzelm 2010-03-02 proper (type_)notation;
2009-11-19 huffman 2009-11-19 add map_ID lemmas
2009-11-09 huffman 2009-11-09 add map_map lemmas
2009-11-05 huffman 2009-11-05 map functions for various types, with ep_pair/deflation/finite_deflation lemmas
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-05-11 huffman 2009-05-11 use Pair/fst/snd instead of cpair/cfst/csnd
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-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-12-11 wenzelm 2008-12-11 pcpodef package: state two goals, instead of encoded conjunction;
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-02-07 huffman 2008-02-07 fix broken syntax translations
2008-01-15 huffman 2008-01-15 add instance for class bifinite
2008-01-10 huffman 2008-01-10 new compactness lemmas; removed duplicated flat_less_iff
2008-01-04 huffman 2008-01-04 new instance proofs for classes finite_po, chfin, flat
2008-01-01 huffman 2008-01-01 add induction rule ssum_induct
2007-12-21 huffman 2007-12-21 changed type definition to make Iwhen and reasoning about chains unnecessary; rearranged sections
2007-10-21 wenzelm 2007-10-21 modernized specifications ('definition', 'abbreviation', 'notation');
2006-04-13 huffman 2006-04-13 add lemma less_UU_iff as default simp rule
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-10-12 huffman 2005-10-12 added compactness lemmas; cleaned up
2005-10-10 huffman 2005-10-10 add names to infix declarations
2005-07-26 huffman 2005-07-26 renamed Exh_Ssum1 to Exh_Ssum; cleaned up
2005-07-14 huffman 2005-07-14 simplified proof of cont_Iwhen3
2005-07-08 huffman 2005-07-08 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
2005-07-07 huffman 2005-07-07 use theorem ch2ch_cont
2005-07-06 huffman 2005-07-06 use new pcpodef package
2005-06-08 huffman 2005-06-08 renamed theorems less_ssum4a,b,c,d to more meaningful names
2005-06-03 huffman 2005-06-03 changed to use new contI; renamed strict, defined, and inject lemmas
2005-05-26 huffman 2005-05-26 added defaultsort declaration, moved cpair_less to Cprod.thy
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 Simplified version of strict sum theory, using TypedefPcpo
2005-03-11 huffman 2005-03-11 simplified some definitions, many proofs are much shorter
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