src/HOL/HOLCF/Completion.thy
2017-04-04 wenzelm 2017-04-04 eliminated Plain_HOLCF.thy (see also 8e92772bc0e8): it was modeled after HOL/Plain.thy which was discontinued later;
2017-04-04 wenzelm 2017-04-04 tuned (see also 1fa1023b13b9);
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-01-13 wenzelm 2016-01-13 isabelle update_cartouches -c -t;
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-02-12 blanchet 2014-02-12 renamed 'nat_{case,rec}' to '{case,rec}_nat'
2013-12-25 haftmann 2013-12-25 prefer more canonical names for lemmas on min/max
2011-03-29 wenzelm 2011-03-29 tuned headers;
2011-01-12 wenzelm 2011-01-12 eliminated global prems;
2010-12-24 huffman 2010-12-24 remove lemma ideal_completion.principal_induct2, use principal_induct twice instead
2010-12-22 huffman 2010-12-22 rename function ideal_completion.basis_fun to ideal_completion.extension
2010-12-15 huffman 2010-12-15 add notsqsubseteq syntax
2010-12-06 huffman 2010-12-06 simplify ideal completion proofs
2010-12-01 huffman 2010-12-01 reformulate lemma preorder.ex_ideal, and use it for typedefs
2010-11-27 huffman 2010-11-27 moved directory src/HOLCF to src/HOL/HOLCF; added HOLCF theories to src/HOL/IsaMakefile;