| Tue, 19 Oct 2004 18:18:45 +0200 |
paulson |
converted some induct_tac to induct
|
file |
diff |
annotate
|
| Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
| Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
| Sat, 05 Jun 2004 13:07:04 +0200 |
wenzelm |
improved symbolic syntax of Eps: \<some> for mode "epsilon";
|
file |
diff |
annotate
|
| Wed, 19 May 2004 11:29:47 +0200 |
paulson |
conversion of Hilbert_Choice to Isar script
|
file |
diff |
annotate
|
| Thu, 19 Feb 2004 16:44:21 +0100 |
ballarin |
New lemmas about inversion of restricted functions.
|
file |
diff |
annotate
|
| Fri, 26 Sep 2003 10:34:57 +0200 |
paulson |
misc tidying
|
file |
diff |
annotate
|
| Thu, 17 Jul 2003 15:23:20 +0200 |
skalberg |
Added package for definition by specification.
|
file |
diff |
annotate
|
| Sun, 22 Dec 2002 15:02:40 +0100 |
nipkow |
removed some problems with print translations
|
file |
diff |
annotate
|
| Sun, 22 Dec 2002 10:43:43 +0100 |
nipkow |
added print translations tha avoid eta contraction for important binders.
|
file |
diff |
annotate
|
| Thu, 26 Sep 2002 10:51:29 +0200 |
paulson |
Converted Fun to Isar style.
|
file |
diff |
annotate
|
| Wed, 05 Dec 2001 03:07:44 +0100 |
wenzelm |
tuned declarations;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2001 18:33:57 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 03 Nov 2001 01:33:54 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2001 21:17:24 +0200 |
wenzelm |
avoid ML bindings;
|
file |
diff |
annotate
|
| Wed, 25 Jul 2001 17:58:26 +0200 |
paulson |
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
|
file |
diff |
annotate
|
| Wed, 25 Jul 2001 13:13:01 +0200 |
paulson |
partial restructuring to reduce dependence on Axiom of Choice
|
file |
diff |
annotate
|