| Fri, 15 Feb 2008 16:09:12 +0100 |
haftmann |
<= and < on nat no longer depend on wellfounded relations
|
file |
diff |
annotate
|
| Thu, 27 Sep 2007 17:55:28 +0200 |
paulson |
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
|
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 23:15:41 +0200 |
huffman |
removed all references to star_n and FreeUltrafilterNat
|
file |
diff |
annotate
|
| Wed, 27 Sep 2006 20:39:09 +0200 |
wenzelm |
removed redundant lemmas;
|
file |
diff |
annotate
|
| Sat, 27 May 2006 17:42:02 +0200 |
wenzelm |
tuned;
|
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
|
| Mon, 12 Sep 2005 23:13:46 +0200 |
huffman |
updated to work with latest HOL-Complex
|
file |
diff |
annotate
|
| Fri, 09 Sep 2005 20:37:00 +0200 |
huffman |
updated to work with new HOL-Complex version
|
file |
diff |
annotate
|
| Fri, 01 Jul 2005 17:41:10 +0200 |
nipkow |
prime is a predicate now.
|
file |
diff |
annotate
|
| Mon, 30 Aug 2004 14:43:29 +0200 |
chaieb |
commentar eliminated a line 156 - arith raised Match exception at m dvd 2
|
file |
diff |
annotate
|
| Thu, 19 Aug 2004 12:35:45 +0200 |
nipkow |
new import syntax
|
file |
diff |
annotate
|
| Fri, 30 Jul 2004 18:37:58 +0200 |
paulson |
conversion of Integration and NSPrimes to Isar scripts
|
file |
diff |
annotate
|
| Wed, 28 May 2003 10:48:20 +0200 |
paulson |
examples now use Complex_Main
|
file |
diff |
annotate
|
| Mon, 05 May 2003 18:22:31 +0200 |
paulson |
new session Complex for the complex numbers
|
file |
diff |
annotate
|