src/HOL/Wellfounded.thy
2016-12-21 haftmann 2016-12-21 dropped aliasses
2016-10-01 wenzelm 2016-10-01 tuned;
2016-09-18 wenzelm 2016-09-18 tuned proofs;
2016-08-05 wenzelm 2016-08-05 misc tuning and modernization;
2016-07-31 wenzelm 2016-07-31 misc tuning and modernization;
2016-05-23 wenzelm 2016-05-23 proper document source; tuned proofs;
2016-05-23 wenzelm 2016-05-23 misc tuning and modernization;
2016-05-17 eberlm 2016-05-17 Moved material from AFP/Randomised_Social_Choice to distribution
2016-05-12 haftmann 2016-05-12 a quasi-recursive characterization of the multiset order (by Christian Sternagel)
2015-12-28 wenzelm 2015-12-28 prefer symbols for "Union", "Inter";
2015-12-27 wenzelm 2015-12-27 discontinued ASCII replacement syntax <*>;
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-10-06 wenzelm 2015-10-06 fewer aliases for toplevel theorem statements;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-06-17 paulson 2015-06-17 New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
2015-04-27 nipkow 2015-04-27 new lemma
2015-03-25 wenzelm 2015-03-25 prefer local fixes;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-07 wenzelm 2014-10-07 more bibtex entries; more antiquotations;
2014-04-23 blanchet 2014-04-23 move size hooks together, with new one preceding old one and sharing same theory data
2014-04-03 blanchet 2014-04-03 use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
2014-03-19 haftmann 2014-03-19 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
2014-03-16 haftmann 2014-03-16 normalising simp rules for compound operators
2014-03-06 blanchet 2014-03-06 renamed 'map_pair' to 'map_prod'
2014-01-17 blanchet 2014-01-17 folded 'Wellfounded_More_FP' into 'Wellfounded'
2013-11-10 haftmann 2013-11-10 qualifed popular user space names
2012-10-20 bulwahn 2012-10-20 adjusting proofs
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-04-03 griff 2012-04-03 renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
2012-03-12 noschinl 2012-03-12 tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
2012-03-12 noschinl 2012-03-12 tuned simpset
2012-02-24 haftmann 2012-02-24 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-24 haftmann 2012-02-24 given up disfruitful branch
2012-02-23 haftmann 2012-02-23 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-01-30 bulwahn 2012-01-30 adding code_unfold to make measure executable
2012-01-28 bulwahn 2012-01-28 reverting 46c2c96f5d92 as it only provides mostly non-terminating executions for generated code
2012-01-25 bulwahn 2012-01-25 adding very basic code generation to Wellfounded theory
2012-01-10 berghofe 2012-01-10 pred_subset_eq and SUP_UN_eq2 are now standard pred_set_conv rules
2011-12-24 haftmann 2011-12-24 adjusted to set/pred distinction by means of type constructor `set`
2011-10-13 haftmann 2011-10-13 moved acyclic predicate up in hierarchy
2011-10-13 haftmann 2011-10-13 modernized definitions
2011-09-20 haftmann 2011-09-20 tuned specification and lemma distribution among theories; tuned proofs
2011-09-15 hoelzl 2011-09-15 removed further legacy rules from Complete_Lattices
2011-09-13 huffman 2011-09-13 tuned proofs
2011-08-11 krauss 2011-08-11 removed unused material, which does not really belong here
2011-06-01 nipkow 2011-06-01 tuned lemmas
2011-06-01 nipkow 2011-06-01 new lemmas
2011-02-08 nipkow 2011-02-08 added termination lemmas
2010-12-08 haftmann 2010-12-08 primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
2010-11-18 haftmann 2010-11-18 map_pair replaces prod_fun
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-06-11 haftmann 2010-06-11 declare lex_prod_def [code del]
2010-05-05 krauss 2010-05-05 repaired comments where SOMEthing went utterly wrong (cf. 2b04504fcb69)
2010-05-04 haftmann 2010-05-04 locale predicates of classes carry a mandatory "class" prefix
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-03-11 haftmann 2010-03-11 Big_Operators now in Main rather than Plain
2010-03-10 haftmann 2010-03-10 split off theory Big_Operators from theory Finite_Set
2010-02-18 huffman 2010-02-18 get rid of many duplicate simp rule warnings