src/HOL/Wellfounded_Recursion.ML
2004-02-19 ballarin 2004-02-19 Efficient, graph-based reasoner for linear and partial orders. + Setup as solver in the HOL simplifier.
2003-03-17 nipkow 2003-03-17 just a few mods to a few thms
2001-12-20 nipkow 2001-12-20 renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
2001-12-13 wenzelm 2001-12-13 isatool expandshort;
2001-07-25 paulson 2001-07-25 partial restructuring to reduce dependence on Axiom of Choice
2001-05-22 berghofe 2001-05-22 Inductive characterization of wfrec combinator.
2001-02-15 oheimb 2001-02-15 supressed some warnings on identical proofstate moved wellorder_LeastI,wellorder_Least_le,wellorder_not_less_Least from Nat.ML to Wellfounded_Recursion.ML added wellorder axclass
2001-01-09 nipkow 2001-01-09 `` -> and ``` -> ``
2000-10-12 nipkow 2000-10-12 *** empty log message ***