src/HOLCF/Pcpodef.thy
2010-03-22 huffman 2010-03-22 remove LaTeX hyperref warnings by avoiding antiquotations within section headings
2009-06-21 haftmann 2009-06-21 discontinued ancient tradition to suffix certain ML module names with "_package"
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-09-02 haftmann 2008-09-02 adapted to class instantiation compliance
2008-06-20 huffman 2008-06-20 moved Abs_image to Typedef.thy; prove finite_UNIV outside the locale
2008-03-27 huffman 2008-03-27 make preorder locale into a superclass of class po
2008-01-31 huffman 2008-01-31 add lemma cpo_lubI
2008-01-18 huffman 2008-01-18 pcpodef generates strict_iff lemmas
2008-01-18 huffman 2008-01-18 change lemma admD to rule_format
2008-01-17 huffman 2008-01-17 change class axiom chfin to rule_format
2008-01-04 huffman 2008-01-04 new instance proofs for classes finite_po, chfin, flat
2007-05-31 wenzelm 2007-05-31 moved HOLCF tools to canonical place;
2006-05-01 huffman 2006-05-01 add theorem typdef_flat
2005-10-11 huffman 2005-10-11 added theorem typedef_compact
2005-10-10 huffman 2005-10-10 added theorem typedef_chfin
2005-07-26 huffman 2005-07-26 cleaned up; renamed some theorems
2005-07-07 huffman 2005-07-07 use theorems ch2ch_cont, cont2contlubE
2005-07-06 huffman 2005-07-06 renamed from TypedefPcpo.thy; added theorems Rep_defined, Abs_defined; uses pcpodef_package.ML