src/HOL/Transitive_Closure.thy
Tue, 07 Jul 2015 18:01:30 +0200 hoelzl add monotonicity rule for rtranclp
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Sun, 22 Jun 2014 12:37:55 +0200 nipkow r_into_(r)trancl should not be [simp]: helps little and comlicates some AFP proofs
Sat, 21 Jun 2014 15:46:52 +0200 nipkow added [simp]
Fri, 06 Jun 2014 10:53:33 +0200 nipkow added lemmas
Sat, 22 Mar 2014 21:40:19 +0100 wenzelm more antiquotations;
Wed, 19 Feb 2014 08:34:33 +0100 blanchet moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
Mon, 17 Feb 2014 13:31:42 +0100 blanchet renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)
Wed, 12 Feb 2014 08:37:06 +0100 blanchet adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
Tue, 12 Nov 2013 19:28:53 +0100 hoelzl add acyclicI_order
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Sun, 23 Dec 2012 19:54:15 +0100 nipkow renamed and added lemmas
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Mon, 16 Apr 2012 17:22:51 +0200 Christian Sternagel duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems")
Tue, 03 Apr 2012 17:26:30 +0900 griff renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
Fri, 30 Mar 2012 09:04:29 +0200 haftmann power on predicate relations
Thu, 01 Mar 2012 19:34:52 +0100 haftmann more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
Fri, 24 Feb 2012 22:46:44 +0100 haftmann moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
Fri, 24 Feb 2012 09:40:02 +0100 haftmann given up disfruitful branch
Thu, 23 Feb 2012 21:25:59 +0100 haftmann moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
Mon, 30 Jan 2012 13:55:26 +0100 bulwahn renaming all lemmas with name rel_pow to relpow
Mon, 30 Jan 2012 13:55:23 +0100 bulwahn adding code generation for relpow by copying the ideas for code generation of funpow
Fri, 27 Jan 2012 17:22:05 +0100 bulwahn new code equation for ntrancl that allows computation of the transitive closure of sets on infinite types as well
Sun, 01 Jan 2012 11:28:45 +0100 haftmann cleanup of code declarations
Sat, 24 Dec 2011 15:53:12 +0100 haftmann tuned layout
Sun, 20 Nov 2011 21:07:10 +0100 wenzelm eliminated obsolete "standard";
Sun, 16 Oct 2011 14:48:00 +0200 haftmann tuned type annnotation
Thu, 13 Oct 2011 23:35:15 +0200 haftmann avoid very specific code equation for card; corrected spelling
Thu, 13 Oct 2011 23:27:46 +0200 haftmann bouned transitive closure
Thu, 13 Oct 2011 23:02:59 +0200 haftmann moved acyclic predicate up in hierarchy
Thu, 13 Oct 2011 22:56:19 +0200 haftmann modernized definitions
Mon, 03 Oct 2011 14:43:13 +0200 bulwahn adding lemma about rel_pow in Transitive_Closure for executable equation of the (refl) transitive closure
Tue, 13 Sep 2011 17:07:33 -0700 huffman tuned proofs
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Wed, 29 Jun 2011 20:39:41 +0200 wenzelm simplified/unified Simplifier.mk_solver;
Fri, 13 May 2011 23:58:40 +0200 wenzelm clarified map_simpset versus Simplifier.map_simpset_global;
Wed, 16 Mar 2011 19:50:56 +0100 nipkow added lemmas
Mon, 21 Feb 2011 10:44:19 +0100 blanchet renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Thu, 01 Jul 2010 16:54:42 +0200 haftmann qualified constants Set.member and Set.Collect
Thu, 10 Jun 2010 12:24:03 +0200 haftmann tuned quotes, antiquotations and whitespace
Thu, 18 Feb 2010 14:21:44 -0800 huffman get rid of many duplicate simp rule warnings
Wed, 27 Jan 2010 14:02:53 +0100 haftmann lemma Image_closed_trancl
Sun, 10 Jan 2010 18:06:30 +0100 berghofe Tuned some proofs; nicer case names for some of the induction / cases rules.
Tue, 24 Nov 2009 10:31:01 +0100 blanchet removed "nitpick_def" attributes from (r)trancl(p), since "Nitpick.thy" overrides these
Fri, 13 Nov 2009 14:03:24 +0100 krauss a few lemmas for point-free reasoning about transitive closure
Fri, 09 Oct 2009 13:40:34 +0200 haftmann simplified proof
Tue, 06 Oct 2009 18:44:06 +0200 haftmann inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
Fri, 18 Sep 2009 09:07:48 +0200 haftmann 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
Mon, 27 Jul 2009 21:47:41 +0200 krauss "more standard" argument order of relation composition (op O)
Sun, 26 Jul 2009 22:28:31 +0200 wenzelm replaced old METAHYPS by FOCUS;
Thu, 09 Jul 2009 17:34:59 +0200 krauss move rel_pow_commute: "R O R ^^ n = R ^^ n O R" to Transitive_Closure
Wed, 17 Jun 2009 15:41:49 +0200 nipkow rtrancl lemmas
Thu, 11 Jun 2009 23:13:02 +0200 bulwahn added lemma
Thu, 11 Jun 2009 22:17:13 +0200 bulwahn added lemma
Mon, 01 Jun 2009 10:02:01 +0200 nipkow new lemma
Fri, 24 Apr 2009 17:45:15 +0200 haftmann funpow and relpow with shared "^^" syntax
Mon, 20 Apr 2009 09:32:40 +0200 haftmann power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
Mon, 16 Mar 2009 18:24:30 +0100 wenzelm simplified method setup;
less more (0) -100 -60 tip