| Mon, 28 Feb 2005 13:10:36 +0100 |
paulson |
unfold theorems for trancl and rtrancl
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
| Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
| Mon, 02 Aug 2004 10:12:02 +0200 |
ballarin |
Documentation added; minor improvements.
|
file |
diff |
annotate
|
| Mon, 26 Jul 2004 15:48:50 +0200 |
ballarin |
New prover for transitive and reflexive-transitive closure of relations.
|
file |
diff |
annotate
|
| Wed, 14 Apr 2004 14:13:05 +0200 |
kleing |
use more symbols in HTML output
|
file |
diff |
annotate
|
| Sat, 21 Feb 2004 08:43:08 +0100 |
nipkow |
Transitive_Closure: added consumes and case_names attributes
|
file |
diff |
annotate
|
| Thu, 19 Feb 2004 15:57:34 +0100 |
ballarin |
Efficient, graph-based reasoner for linear and partial orders.
|
file |
diff |
annotate
|
| Mon, 26 Jan 2004 10:34:02 +0100 |
schirmer |
* Support for raw latex output in control symbols: \<^raw...>
|
file |
diff |
annotate
|
| Mon, 05 Jan 2004 00:46:06 +0100 |
nipkow |
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
|
file |
diff |
annotate
|
| Fri, 26 Sep 2003 10:34:57 +0200 |
paulson |
misc tidying
|
file |
diff |
annotate
|
| Mon, 17 Mar 2003 18:38:50 +0100 |
nipkow |
just a few mods to a few thms
|
file |
diff |
annotate
|
| Wed, 27 Nov 2002 17:07:05 +0100 |
berghofe |
Replaced some blasts by rules.
|
file |
diff |
annotate
|
| Wed, 13 Nov 2002 15:24:42 +0100 |
berghofe |
Transitive closure is now defined inductively as well.
|
file |
diff |
annotate
|
| Mon, 25 Feb 2002 20:48:14 +0100 |
wenzelm |
clarified syntax of ``long'' statements: fixes/assumes/shows;
|
file |
diff |
annotate
|
| Mon, 21 Jan 2002 14:45:00 +0100 |
berghofe |
Made some proofs constructive.
|
file |
diff |
annotate
|
| Wed, 09 Jan 2002 17:48:40 +0100 |
wenzelm |
converted theory Transitive_Closure;
|
file |
diff |
annotate
|
| Thu, 20 Dec 2001 18:22:44 +0100 |
nipkow |
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
|
file |
diff |
annotate
|
| Sun, 09 Dec 2001 14:34:18 +0100 |
kleing |
setup [trans] rules for calculational Isar reasoning
|
file |
diff |
annotate
|
| Tue, 22 May 2001 15:12:11 +0200 |
berghofe |
Transitive closure is now defined via "inductive".
|
file |
diff |
annotate
|
| Wed, 14 Feb 2001 12:16:32 +0100 |
paulson |
a new theorem from Bryan Ford
|
file |
diff |
annotate
|
| Fri, 09 Feb 2001 23:48:50 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 09 Feb 2001 11:40:10 +0100 |
wenzelm |
unsymbolized;
|
file |
diff |
annotate
|
| Mon, 29 Jan 2001 23:02:21 +0100 |
nipkow |
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
|
file |
diff |
annotate
|
| Fri, 26 Jan 2001 00:15:36 +0100 |
wenzelm |
Transitive_Closure turned into new-style theory;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2001 12:11:56 +0100 |
wenzelm |
syntax (xsymbols);
|
file |
diff |
annotate
|
| Fri, 01 Dec 2000 19:41:09 +0100 |
wenzelm |
superscripts: syntax (latex);
|
file |
diff |
annotate
|
| Wed, 25 Oct 2000 18:32:02 +0200 |
wenzelm |
more "xsymbols" syntax;
|
file |
diff |
annotate
|
| Thu, 12 Oct 2000 18:44:35 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|