src/HOL/Transitive_Closure.thy
2015-12-28 wenzelm 2015-12-28 former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-15 wenzelm 2015-11-15 option "inductive_defs" controls exposure of def and mono facts;
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2015-08-27 haftmann 2015-08-27 standardized some occurences of ancient "split" alias
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-07-07 hoelzl 2015-07-07 add monotonicity rule for rtranclp
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-06-22 nipkow 2014-06-22 r_into_(r)trancl should not be [simp]: helps little and comlicates some AFP proofs
2014-06-21 nipkow 2014-06-21 added [simp]
2014-06-06 nipkow 2014-06-06 added lemmas
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2014-02-19 blanchet 2014-02-19 moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
2014-02-17 blanchet 2014-02-17 renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)
2014-02-12 blanchet 2014-02-12 adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
2013-11-12 hoelzl 2013-11-12 add acyclicI_order
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
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