src/HOL/Transitive_Closure.thy
2012-12-23 nipkow 2012-12-23 renamed and added lemmas
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-04-16 Christian Sternagel 2012-04-16 duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
2012-04-03 griff 2012-04-03 renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
2012-03-30 haftmann 2012-03-30 power on predicate relations
2012-03-01 haftmann 2012-03-01 more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
2012-02-24 haftmann 2012-02-24 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-24 haftmann 2012-02-24 given up disfruitful branch
2012-02-23 haftmann 2012-02-23 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-01-30 bulwahn 2012-01-30 renaming all lemmas with name rel_pow to relpow
2012-01-30 bulwahn 2012-01-30 adding code generation for relpow by copying the ideas for code generation of funpow
2012-01-27 bulwahn 2012-01-27 new code equation for ntrancl that allows computation of the transitive closure of sets on infinite types as well
2012-01-01 haftmann 2012-01-01 cleanup of code declarations
2011-12-24 haftmann 2011-12-24 tuned layout
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-10-16 haftmann 2011-10-16 tuned type annnotation
2011-10-13 haftmann 2011-10-13 avoid very specific code equation for card; corrected spelling
2011-10-13 haftmann 2011-10-13 bouned transitive closure
2011-10-13 haftmann 2011-10-13 moved acyclic predicate up in hierarchy
2011-10-13 haftmann 2011-10-13 modernized definitions
2011-10-03 bulwahn 2011-10-03 adding lemma about rel_pow in Transitive_Closure for executable equation of the (refl) transitive closure
2011-09-13 huffman 2011-09-13 tuned proofs
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-06-29 wenzelm 2011-06-29 simplified/unified Simplifier.mk_solver;
2011-05-13 wenzelm 2011-05-13 clarified map_simpset versus Simplifier.map_simpset_global;
2011-03-16 nipkow 2011-03-16 added lemmas
2011-02-21 blanchet 2011-02-21 renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
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-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-07-01 haftmann 2010-07-01 qualified constants Set.member and Set.Collect
2010-06-10 haftmann 2010-06-10 tuned quotes, antiquotations and whitespace
2010-02-18 huffman 2010-02-18 get rid of many duplicate simp rule warnings
2010-01-27 haftmann 2010-01-27 lemma Image_closed_trancl
2010-01-10 berghofe 2010-01-10 Tuned some proofs; nicer case names for some of the induction / cases rules.
2009-11-24 blanchet 2009-11-24 removed "nitpick_def" attributes from (r)trancl(p), since "Nitpick.thy" overrides these
2009-11-13 krauss 2009-11-13 a few lemmas for point-free reasoning about transitive closure
2009-10-09 haftmann 2009-10-09 simplified proof
2009-10-06 haftmann 2009-10-06 inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
2009-09-18 haftmann 2009-09-18 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 krauss 2009-07-27 "more standard" argument order of relation composition (op O)
2009-07-26 wenzelm 2009-07-26 replaced old METAHYPS by FOCUS; eliminated homegrown SUBGOAL combinator -- beware of exception Subscript in body; modernized functor names; minimal tuning of sources; reactivated dead quasi.ML (ever used?);
2009-07-09 krauss 2009-07-09 move rel_pow_commute: "R O R ^^ n = R ^^ n O R" to Transitive_Closure
2009-06-17 nipkow 2009-06-17 rtrancl lemmas
2009-06-11 bulwahn 2009-06-11 added lemma
2009-06-11 bulwahn 2009-06-11 added lemma
2009-06-01 nipkow 2009-06-01 new lemma
2009-04-24 haftmann 2009-04-24 funpow and relpow with shared "^^" syntax
2009-04-20 haftmann 2009-04-20 power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
2009-03-16 wenzelm 2009-03-16 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-02 nipkow 2009-03-02 name changes
2009-02-26 berghofe 2009-02-26 Fixed nonexhaustive match problem in decomp, to make it fail more gracefully in case assumptions are not of the form (Trueprop $ ...).
2009-01-21 haftmann 2009-01-21 changed import hierarchy
2008-05-07 berghofe 2008-05-07 - Function dec in Trancl_Tac must eta-contract relation before calling decr, since it is now a function and could therefore be in eta-expanded form - The trancl prover now does more eta-contraction itself, so eta-contraction is no longer necessary in Tranclp_tac.
2008-03-19 wenzelm 2008-03-19 more antiquotations; eliminated change_claset/simpset;
2008-03-14 nipkow 2008-03-14 Added lemmas
2008-02-28 wenzelm 2008-02-28 rtranclp_induct, tranclp_induct: added case_names; tuned proofs;
2008-02-28 wenzelm 2008-02-28 rtranclE, tranclE: tuned statement, added case_names;