src/HOL/Wellfounded.thy
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
2009-03-11 haftmann 2009-03-11 explicit code equations for some rarely used pred operations
2009-01-21 haftmann 2009-01-21 changed import hierarchy
2009-01-21 haftmann 2009-01-21 dropped ID
2008-12-16 krauss 2008-12-16 method "sizechange" proves termination of functions; added more infrastructure for termination proofs
2008-11-18 krauss 2008-11-18 removed lemmas called lemma1 and lemma2
2008-11-12 krauss 2008-11-12 min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-10-07 haftmann 2008-10-07 arbitrary is undefined
2008-09-17 krauss 2008-09-17 wf_finite_psubset[simp], in_finite_psubset[simp]
2008-08-11 haftmann 2008-08-11 moved class wellorder to theory Orderings
2008-05-23 krauss 2008-05-23 rearranged subsections
2008-05-07 berghofe 2008-05-07 - Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the to_set and to_pred attributes, because it is no longer applied automatically - Manually applied predicate1I in proof of accp_subset, because it is no longer part of the claset - Replaced psubset_def by less_le
2008-04-25 krauss 2008-04-25 Merged theories about wellfoundedness into one: Wellfounded.thy