2011-10-16 ago tuned type annnotation
2011-10-13 ago avoid very specific code equation for card; corrected spelling
2011-10-13 ago bouned transitive closure
2011-10-13 ago moved acyclic predicate up in hierarchy
2011-10-13 ago modernized definitions
2011-10-03 ago adding lemma about rel_pow in Transitive_Closure for executable equation of the (refl) transitive closure
2011-09-13 ago tuned proofs
2011-09-12 ago new fastforce replacing fastsimp - less confusing name
2011-06-29 ago simplified/unified Simplifier.mk_solver;
2011-05-13 ago clarified map_simpset versus Simplifier.map_simpset_global;
2011-03-16 ago added lemmas
2011-02-21 ago renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
2010-09-13 ago renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 ago expand_fun_eq -> ext_iff
2010-07-01 ago qualified constants Set.member and Set.Collect
2010-06-10 ago tuned quotes, antiquotations and whitespace
2010-02-18 ago get rid of many duplicate simp rule warnings
2010-01-27 ago lemma Image_closed_trancl
2010-01-10 ago Tuned some proofs; nicer case names for some of the induction / cases rules.
2009-11-24 ago removed "nitpick_def" attributes from (r)trancl(p), since "Nitpick.thy" overrides these
2009-11-13 ago a few lemmas for point-free reasoning about transitive closure
2009-10-09 ago simplified proof
2009-10-06 ago inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
2009-09-18 ago be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
2009-07-27 ago "more standard" argument order of relation composition (op O)
2009-07-26 ago replaced old METAHYPS by FOCUS;
2009-07-09 ago move rel_pow_commute: "R O R ^^ n = R ^^ n O R" to Transitive_Closure
2009-06-17 ago rtrancl lemmas
2009-06-11 ago added lemma
2009-06-11 ago added lemma
2009-06-01 ago new lemma
2009-04-24 ago funpow and relpow with shared "^^" syntax
2009-04-20 ago power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
2009-03-16 ago simplified method setup;
2009-03-13 ago unified type Proof.method and pervasive METHOD combinators;
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-03-02 ago name changes
2009-02-26 ago Fixed nonexhaustive match problem in decomp, to make it fail more gracefully
2009-01-21 ago changed import hierarchy
2008-05-07 ago - Function dec in Trancl_Tac must eta-contract relation before calling
2008-03-19 ago more antiquotations;
2008-03-14 ago Added lemmas
2008-02-28 ago rtranclp_induct, tranclp_induct: added case_names;
2008-02-28 ago rtranclE, tranclE: tuned statement, added case_names;
2007-11-13 ago Removed some case_names and consumes attributes that are now no longer
2007-11-05 ago tranclD2 (tranclD at the other end) + trancl_power
2007-07-11 ago rtrancl and trancl are now defined using inductive_set.
2007-03-09 ago stepping towards uniform lattice theory development in HOL
2007-02-07 ago Adapted to new inductive definition package.
2007-01-24 ago some new lemmas
2007-01-17 ago induction rules for trancl/rtrancl expressed using subsets
2006-11-29 ago simplified method setup;
2006-11-17 ago more robust syntax for definition/abbreviation/notation;
2006-11-07 ago renamed 'const_syntax' to 'notation';
2006-09-26 ago Changed precedence of "op O" (relation composition) from 60 to 75.
2006-05-16 ago tuned concrete syntax -- abbreviation/const_syntax;
2006-05-12 ago added lemma in_measure
2006-03-10 ago added many simple lemmas
2005-12-08 ago tuned proofs;