src/HOL/HOLCF/Universal.thy
23 months ago wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2017-04-22 wenzelm 2017-04-22 theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-02-23 nipkow 2016-02-23 more canonical names
2016-01-13 wenzelm 2016-01-13 isabelle update_cartouches -c -t;
2015-11-09 wenzelm 2015-11-09 qualifier is mandatory by default;
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-03-10 paulson 2015-03-10 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
2015-03-09 paulson 2015-03-09 Removed the infix operator "choose" to allow HOLCF to build
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-03-13 nipkow 2014-03-13 enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
2013-12-25 haftmann 2013-12-25 prefer more canonical names for lemmas on min/max
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-03-11 wenzelm 2012-03-11 eliminated old-fashioned 'constrains' element;
2011-03-29 wenzelm 2011-03-29 tuned headers;
2011-01-12 wenzelm 2011-01-12 eliminated global prems;
2011-01-04 huffman 2011-01-04 change some lemma names containing 'UU' to 'bottom'
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-12-22 huffman 2010-12-22 rename function ideal_completion.basis_fun to ideal_completion.extension
2010-12-21 huffman 2010-12-21 declare more simp rules, rewrite proofs in Isar-style
2010-12-19 huffman 2010-12-19 types -> type_synonym
2010-12-19 huffman 2010-12-19 reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
2010-12-15 huffman 2010-12-15 add notsqsubseteq syntax
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;