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