src/HOL/Transitive_Closure.thy
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
Fri, 10 Mar 2006 00:53:28 +0100 huffman added many simple lemmas
Thu, 08 Dec 2005 20:15:50 +0100 wenzelm tuned proofs;
Mon, 17 Oct 2005 23:10:13 +0200 wenzelm change_claset/simpset;
Thu, 22 Sep 2005 23:56:15 +0200 nipkow renamed rules to iprover
Tue, 21 Jun 2005 11:08:31 +0200 kleing lemma, equation between rtrancl and trancl
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Thu, 21 Apr 2005 22:02:06 +0200 wenzelm superceded by Pure.thy and CPure.thy;
Mon, 28 Feb 2005 13:10:36 +0100 paulson unfold theorems for trancl and rtrancl
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Wed, 18 Aug 2004 11:09:40 +0200 nipkow import -> imports
Mon, 16 Aug 2004 14:22:27 +0200 nipkow New theory header syntax.
Mon, 02 Aug 2004 10:12:02 +0200 ballarin Documentation added; minor improvements.
Mon, 26 Jul 2004 15:48:50 +0200 ballarin New prover for transitive and reflexive-transitive closure of relations.
Wed, 14 Apr 2004 14:13:05 +0200 kleing use more symbols in HTML output
Sat, 21 Feb 2004 08:43:08 +0100 nipkow Transitive_Closure: added consumes and case_names attributes
Thu, 19 Feb 2004 15:57:34 +0100 ballarin Efficient, graph-based reasoner for linear and partial orders.
Mon, 26 Jan 2004 10:34:02 +0100 schirmer * Support for raw latex output in control symbols: \<^raw...>
Mon, 05 Jan 2004 00:46:06 +0100 nipkow undid split_comp_eq[simp] because it leads to nontermination together with split_def!
less more (0) -60 tip