src/HOL/Transitive_Closure.thy
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;
Fri, 13 Mar 2009 19:58:26 +0100 wenzelm unified type Proof.method and pervasive METHOD combinators;
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Mon, 02 Mar 2009 16:53:55 +0100 nipkow name changes
Thu, 26 Feb 2009 16:32:46 +0100 berghofe Fixed nonexhaustive match problem in decomp, to make it fail more gracefully
Wed, 21 Jan 2009 23:40:23 +0100 haftmann changed import hierarchy
Wed, 07 May 2008 10:56:49 +0200 berghofe - Function dec in Trancl_Tac must eta-contract relation before calling
Wed, 19 Mar 2008 22:47:38 +0100 wenzelm more antiquotations;
Fri, 14 Mar 2008 19:57:12 +0100 nipkow Added lemmas
Thu, 28 Feb 2008 15:54:37 +0100 wenzelm rtranclp_induct, tranclp_induct: added case_names;
Thu, 28 Feb 2008 12:56:28 +0100 wenzelm rtranclE, tranclE: tuned statement, added case_names;
Tue, 13 Nov 2007 11:02:55 +0100 berghofe Removed some case_names and consumes attributes that are now no longer
Mon, 05 Nov 2007 22:48:37 +0100 kleing tranclD2 (tranclD at the other end) + trancl_power
Wed, 11 Jul 2007 11:10:37 +0200 berghofe rtrancl and trancl are now defined using inductive_set.
Fri, 09 Mar 2007 08:45:50 +0100 haftmann stepping towards uniform lattice theory development in HOL
Wed, 07 Feb 2007 17:28:09 +0100 berghofe Adapted to new inductive definition package.
Wed, 24 Jan 2007 17:10:50 +0100 paulson some new lemmas
Wed, 17 Jan 2007 09:53:50 +0100 paulson induction rules for trancl/rtrancl expressed using subsets
Wed, 29 Nov 2006 15:44:56 +0100 wenzelm simplified method setup;
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Tue, 07 Nov 2006 11:47:57 +0100 wenzelm renamed 'const_syntax' to 'notation';
Tue, 26 Sep 2006 17:33:04 +0200 krauss Changed precedence of "op O" (relation composition) from 60 to 75.
Tue, 16 May 2006 21:33:01 +0200 wenzelm tuned concrete syntax -- abbreviation/const_syntax;
Fri, 12 May 2006 11:19:41 +0200 nipkow added lemma in_measure
less more (0) -60 tip