src/HOL/Wellfounded.thy
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