src/HOL/Transitive_Closure.thy
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;
2007-11-13 berghofe 2007-11-13 Removed some case_names and consumes attributes that are now no longer needed due to changes in the to_pred and to_set attributes.
2007-11-05 kleing 2007-11-05 tranclD2 (tranclD at the other end) + trancl_power
2007-07-11 berghofe 2007-07-11 rtrancl and trancl are now defined using inductive_set.
2007-03-09 haftmann 2007-03-09 stepping towards uniform lattice theory development in HOL
2007-02-07 berghofe 2007-02-07 Adapted to new inductive definition package.
2007-01-24 paulson 2007-01-24 some new lemmas
2007-01-17 paulson 2007-01-17 induction rules for trancl/rtrancl expressed using subsets
2006-11-29 wenzelm 2006-11-29 simplified method setup; reactivated dead code;
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-07 wenzelm 2006-11-07 renamed 'const_syntax' to 'notation';
2006-09-26 krauss 2006-09-26 Changed precedence of "op O" (relation composition) from 60 to 75.
2006-05-16 wenzelm 2006-05-16 tuned concrete syntax -- abbreviation/const_syntax;
2006-05-12 nipkow 2006-05-12 added lemma in_measure
2006-03-10 huffman 2006-03-10 added many simple lemmas
2005-12-08 wenzelm 2005-12-08 tuned proofs;
2005-10-17 wenzelm 2005-10-17 change_claset/simpset;
2005-09-22 nipkow 2005-09-22 renamed rules to iprover
2005-06-21 kleing 2005-06-21 lemma, equation between rtrancl and trancl
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-04-21 wenzelm 2005-04-21 superceded by Pure.thy and CPure.thy;
2005-02-28 paulson 2005-02-28 unfold theorems for trancl and rtrancl
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-08-02 ballarin 2004-08-02 Documentation added; minor improvements.
2004-07-26 ballarin 2004-07-26 New prover for transitive and reflexive-transitive closure of relations. - Code in Provers/trancl.ML - HOL: Simplifier set up to use it as solver
2004-04-14 kleing 2004-04-14 use more symbols in HTML output