| Fri, 09 Mar 2007 08:45:50 +0100 |
haftmann |
stepping towards uniform lattice theory development in HOL
|
file |
diff |
annotate
|
| Wed, 07 Feb 2007 17:28:09 +0100 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
| Wed, 24 Jan 2007 17:10:50 +0100 |
paulson |
some new lemmas
|
file |
diff |
annotate
|
| Wed, 17 Jan 2007 09:53:50 +0100 |
paulson |
induction rules for trancl/rtrancl expressed using subsets
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 15:44:56 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 11:47:57 +0100 |
wenzelm |
renamed 'const_syntax' to 'notation';
|
file |
diff |
annotate
|
| Tue, 26 Sep 2006 17:33:04 +0200 |
krauss |
Changed precedence of "op O" (relation composition) from 60 to 75.
|
file |
diff |
annotate
|
| Tue, 16 May 2006 21:33:01 +0200 |
wenzelm |
tuned concrete syntax -- abbreviation/const_syntax;
|
file |
diff |
annotate
|
| Fri, 12 May 2006 11:19:41 +0200 |
nipkow |
added lemma in_measure
|
file |
diff |
annotate
|
| Fri, 10 Mar 2006 00:53:28 +0100 |
huffman |
added many simple lemmas
|
file |
diff |
annotate
|
| Thu, 08 Dec 2005 20:15:50 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 17 Oct 2005 23:10:13 +0200 |
wenzelm |
change_claset/simpset;
|
file |
diff |
annotate
|
| Thu, 22 Sep 2005 23:56:15 +0200 |
nipkow |
renamed rules to iprover
|
file |
diff |
annotate
|
| Tue, 21 Jun 2005 11:08:31 +0200 |
kleing |
lemma, equation between rtrancl and trancl
|
file |
diff |
annotate
|