src/HOL/Wellfounded_Relations.ML
2003-03-17 nipkow 2003-03-17 just a few mods to a few thms
2001-12-17 nipkow 2001-12-17 mods due to mor powerful simprocs for 1-point rules (quantifier1).
2001-12-13 wenzelm 2001-12-13 isatool expandshort;
2001-07-25 paulson 2001-07-25 Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
2001-05-31 oheimb 2001-05-31 added same_fstI as safe intro rule
2001-02-20 oheimb 2001-02-20 added same_fstI
2001-02-15 oheimb 2001-02-15 moved inv_image to Relation nonempty_has_least of Nat.ML -> ex_has_least_nat of Wellfounded_Relations.ML added wf_linord_ex_has_least,LeastM_nat_lemma,LeastM_natI,LeastM_nat_le
2001-01-29 nipkow 2001-01-29 Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
2000-12-13 nipkow 2000-12-13 small mods.
2000-10-17 paulson 2000-10-17 renaming of contrapos rules
2000-10-12 nipkow 2000-10-12 *** empty log message ***