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