src/HOLCF/Ssum.thy
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