src/HOL/Wellfounded.thy
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
2009-10-26 krauss 2009-10-26 authentic constants; moved "acyclic" further down
2009-10-26 krauss 2009-10-26 point-free characterization of well-foundedness
2009-10-26 krauss 2009-10-26 replaced (outdated) comments by explicit statements
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-09-23 haftmann 2009-09-23 simplified proof
2009-08-31 krauss 2009-08-31 moved lemma Wellfounded.in_inv_image to Relation.thy
2009-08-31 krauss 2009-08-31 moved wfrec to Recdef.thy
2009-08-31 krauss 2009-08-31 no consts_code for wfrec, as it violates the "code generation = equational reasoning" principle
2009-07-28 haftmann 2009-07-28 explicit is better than implicit
2009-07-28 krauss 2009-07-28 moved obsolete same_fst to Recdef.thy
2009-07-27 krauss 2009-07-27 "more standard" argument order of relation composition (op O)
2009-07-25 haftmann 2009-07-25 explicit is better than implicit
2009-06-23 haftmann 2009-06-23 uniformly capitialized names for subdirectories
2009-04-26 haftmann 2009-04-26 reverted slip in theory imports
2009-04-26 haftmann 2009-04-26 adjusted to changes in power syntax