| Wed, 07 May 2008 10:57:19 +0200 |
berghofe |
Adapted to encoding of sets as predicates
|
file |
diff |
annotate
|
| Mon, 03 Mar 2008 15:37:14 +0100 |
haftmann |
continued localization
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 15:14:02 +0100 |
haftmann |
splitted class uminus from class minus
|
file |
diff |
annotate
|
| Thu, 13 Dec 2007 07:09:23 +0100 |
haftmann |
changed order in class parameters
|
file |
diff |
annotate
|
| Tue, 11 Dec 2007 10:23:08 +0100 |
haftmann |
joined StarClasses theory with StarDef
|
file |
diff |
annotate
|
| Tue, 19 Dec 2006 19:34:35 +0100 |
huffman |
add lemmas Standard_starfun(2)_iff
|
file |
diff |
annotate
|
| Tue, 12 Dec 2006 07:46:40 +0100 |
huffman |
consistent naming for FreeUltrafilterNat lemmas; cleaned up
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Wed, 27 Sep 2006 00:54:10 +0200 |
huffman |
define new constant Standard = range star_of
|
file |
diff |
annotate
|
| Mon, 03 Jul 2006 20:03:11 +0200 |
nipkow |
replaced respects2 by congruent2 because of type problem
|
file |
diff |
annotate
|
| Fri, 02 Jun 2006 23:22:29 +0200 |
wenzelm |
misc cleanup;
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
| Sat, 17 Sep 2005 01:50:01 +0200 |
huffman |
use interpretation command
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 23:46:22 +0200 |
huffman |
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
|
file |
diff |
annotate
|