| 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
|