2010-10-07 huffman 2010-10-07 move stuff from Algebraic.thy to Bifinite.thy and elsewhere
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;
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
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
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-01-15 huffman 2008-01-15 clean up some proofs; add lemmas spair_strict_iff, spair_less_iff, spair_eq_iff; add instance for class bifinite
2008-01-10 huffman 2008-01-10 Compactness subsection with new lemmas
2008-01-04 huffman 2008-01-04 new instance proofs for classes finite_po, chfin, flat
2008-01-01 huffman 2008-01-01 declare sprodE as cases rule; new induction rule sprod_induct
2007-10-21 wenzelm 2007-10-21 modernized specifications ('definition', 'axiomatization');
2007-10-21 wenzelm 2007-10-21 modernized specifications ('definition', 'abbreviation', 'notation');
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 cleaned up
2005-07-12 huffman 2005-07-12 added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
2005-07-08 huffman 2005-07-08 add lemma eq_sprod
2005-07-06 huffman 2005-07-06 use new pcpodef package
2005-06-23 huffman 2005-06-23 add csplit3, ssplit3, fup3 as simp rules
2005-06-08 huffman 2005-06-08 added theorems less_sprod, spair_less, spair_eq, spair_inject
2005-06-03 huffman 2005-06-03 renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
2005-05-26 huffman 2005-05-26 added defaultsort declaration
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 product theory, using TypedefPcpo
2005-05-06 huffman 2005-05-06 Replaced all unnecessary uses of SOME with THE or LEAST
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