| Wed, 11 Jul 2007 11:01:24 +0200 |
berghofe |
top and bot are now constants.
|
file |
diff |
annotate
|
| Tue, 10 Jul 2007 17:30:47 +0200 |
haftmann |
moved lfp_induct2 to Relation.thy
|
file |
diff |
annotate
|
| Wed, 30 May 2007 21:09:12 +0200 |
haftmann |
generalized lemmas
|
file |
diff |
annotate
|
| Fri, 25 May 2007 21:08:52 +0200 |
haftmann |
using rudimentary class target mechanism
|
file |
diff |
annotate
|
| Thu, 10 May 2007 10:21:47 +0200 |
haftmann |
localized Sup/Inf
|
file |
diff |
annotate
|
| Sun, 06 May 2007 21:50:17 +0200 |
haftmann |
changed code generator invocation syntax
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 11:21:42 +0200 |
haftmann |
Isar definitions are now added explicitly to code theorem table
|
file |
diff |
annotate
|
| Tue, 20 Mar 2007 08:27:22 +0100 |
haftmann |
new lemmas
|
file |
diff |
annotate
|
| Fri, 16 Mar 2007 21:32:08 +0100 |
haftmann |
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
|
file |
diff |
annotate
|
| Mon, 12 Mar 2007 19:23:49 +0100 |
wenzelm |
syntax: proper body priorty for derived binders;
|
file |
diff |
annotate
|
| Sat, 10 Mar 2007 16:23:28 +0100 |
berghofe |
Generalized version of SUP and INF (with index set).
|
file |
diff |
annotate
|
| Fri, 09 Mar 2007 08:45:50 +0100 |
haftmann |
stepping towards uniform lattice theory development in HOL
|
file |
diff |
annotate
|
| Fri, 02 Mar 2007 15:43:21 +0100 |
haftmann |
now using "class"
|
file |
diff |
annotate
|
| Mon, 26 Feb 2007 15:08:37 +0100 |
krauss |
Added lemma lfp_const: "lfp (%x. t) = t
|
file |
diff |
annotate
|
| Wed, 07 Feb 2007 17:59:40 +0100 |
berghofe |
Introduction and elimination rules for <= on predicates
|
file |
diff |
annotate
|
| Mon, 27 Nov 2006 13:42:39 +0100 |
haftmann |
moved order arities for fun and bool to Fun/Orderings
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Mon, 13 Nov 2006 15:43:03 +0100 |
haftmann |
added LOrder dependency
|
file |
diff |
annotate
|
| Sun, 12 Nov 2006 21:31:52 +0100 |
nipkow |
image_constant_conv no longer [simp]
|
file |
diff |
annotate
|
| Sun, 12 Nov 2006 19:22:10 +0100 |
nipkow |
started reorgnization of lattice theories
|
file |
diff |
annotate
|
| Fri, 13 Oct 2006 18:10:16 +0200 |
berghofe |
Generalized gfp and lfp to arbitrary complete lattices.
|
file |
diff |
annotate
|
| Thu, 22 Sep 2005 23:56:15 +0200 |
nipkow |
renamed rules to iprover
|
file |
diff |
annotate
|
| Wed, 03 Aug 2005 14:47:51 +0200 |
avigad |
combined Lfp and Gfp to FixedPoint
|
file |
diff |
annotate
|