src/HOL/Transitive_Closure.thy
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!
Fri, 26 Sep 2003 10:34:57 +0200 paulson misc tidying
Mon, 17 Mar 2003 18:38:50 +0100 nipkow just a few mods to a few thms
Wed, 27 Nov 2002 17:07:05 +0100 berghofe Replaced some blasts by rules.
Wed, 13 Nov 2002 15:24:42 +0100 berghofe Transitive closure is now defined inductively as well.
Mon, 25 Feb 2002 20:48:14 +0100 wenzelm clarified syntax of ``long'' statements: fixes/assumes/shows;
Mon, 21 Jan 2002 14:45:00 +0100 berghofe Made some proofs constructive.
Wed, 09 Jan 2002 17:48:40 +0100 wenzelm converted theory Transitive_Closure;
Thu, 20 Dec 2001 18:22:44 +0100 nipkow renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
Sun, 09 Dec 2001 14:34:18 +0100 kleing setup [trans] rules for calculational Isar reasoning
Tue, 22 May 2001 15:12:11 +0200 berghofe Transitive closure is now defined via "inductive".
Wed, 14 Feb 2001 12:16:32 +0100 paulson a new theorem from Bryan Ford
Fri, 09 Feb 2001 23:48:50 +0100 wenzelm tuned;
Fri, 09 Feb 2001 11:40:10 +0100 wenzelm unsymbolized;
Mon, 29 Jan 2001 23:02:21 +0100 nipkow Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
Fri, 26 Jan 2001 00:15:36 +0100 wenzelm Transitive_Closure turned into new-style theory;
Tue, 09 Jan 2001 12:11:56 +0100 wenzelm syntax (xsymbols);
Fri, 01 Dec 2000 19:41:09 +0100 wenzelm superscripts: syntax (latex);
Wed, 25 Oct 2000 18:32:02 +0200 wenzelm more "xsymbols" syntax;
Thu, 12 Oct 2000 18:44:35 +0200 nipkow *** empty log message ***
less more (0) tip