| Mon, 09 Dec 2002 10:38:56 +0100 |
ballarin |
Fixed bug in simpdata.ML that prevented the use of congruence rules from a
|
changeset |
files
|
| Fri, 06 Dec 2002 15:16:30 +0100 |
oheimb |
corrected swallowing of newlines after end-of-ignore
|
changeset |
files
|
| Fri, 06 Dec 2002 11:09:02 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Thu, 05 Dec 2002 18:44:16 +0100 |
kleing |
for dvi target
|
changeset |
files
|
| Thu, 05 Dec 2002 17:12:07 +0100 |
kleing |
exercise collection
|
changeset |
files
|
| Fri, 29 Nov 2002 14:26:55 +0100 |
ballarin |
Incompatibility with SML/NJ fixed.
|
changeset |
files
|
| Fri, 29 Nov 2002 09:48:28 +0100 |
nipkow |
added a few lemmas
|
changeset |
files
|
| Thu, 28 Nov 2002 15:44:34 +0100 |
ballarin |
Transitivity reasoner renamed to linorder.ML. README updated.
|
changeset |
files
|
| Thu, 28 Nov 2002 10:50:42 +0100 |
ballarin |
HOL-Algebra partially ported to Isar.
|
changeset |
files
|
| Wed, 27 Nov 2002 17:25:41 +0100 |
berghofe |
prop_of now returns proposition in beta-eta normal form.
|
changeset |
files
|
| Wed, 27 Nov 2002 17:25:04 +0100 |
berghofe |
- tuned beta_eta_convert
|
changeset |
files
|
| Wed, 27 Nov 2002 17:23:19 +0100 |
berghofe |
Correctness proofs are now modular, too.
|
changeset |
files
|
| Wed, 27 Nov 2002 17:22:18 +0100 |
berghofe |
Parameters in definitions are now renamed to avoid clashes with
|
changeset |
files
|
| Wed, 27 Nov 2002 17:20:49 +0100 |
berghofe |
default_output now escapes \'s more carefully.
|
changeset |
files
|
| Wed, 27 Nov 2002 17:17:53 +0100 |
berghofe |
Added XML parser (useful for parsing PGIP / PGML).
|
changeset |
files
|
| Wed, 27 Nov 2002 17:16:47 +0100 |
berghofe |
Added some functions for processing PGIP (thanks to David Aspinall).
|
changeset |
files
|
| Wed, 27 Nov 2002 17:11:38 +0100 |
berghofe |
Fixed bug in consts_code section.
|
changeset |
files
|
| Wed, 27 Nov 2002 17:07:05 +0100 |
berghofe |
Replaced some blasts by rules.
|
changeset |
files
|
| Wed, 27 Nov 2002 17:06:47 +0100 |
berghofe |
Changed format of realizers / correctness proofs.
|
changeset |
files
|
| Mon, 25 Nov 2002 20:32:29 +0100 |
nipkow |
renamed a few constants
|
changeset |
files
|
| Thu, 21 Nov 2002 17:40:11 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 20 Nov 2002 10:43:20 +0100 |
paulson |
textual tweak
|
changeset |
files
|
| Tue, 19 Nov 2002 10:41:20 +0100 |
paulson |
stylistic tweaks
|
changeset |
files
|
| Mon, 18 Nov 2002 14:51:44 +0100 |
nipkow |
beautification
|
changeset |
files
|
| Sun, 17 Nov 2002 23:43:53 +0100 |
berghofe |
Fixed small bug that caused some definitions to be "forgotten".
|
changeset |
files
|
| Sat, 16 Nov 2002 23:01:59 +0100 |
kleing |
beautified "match"
|
changeset |
files
|
| Sat, 16 Nov 2002 22:54:39 +0100 |
kleing |
beautified "match"
|
changeset |
files
|
| Fri, 15 Nov 2002 18:02:25 +0100 |
nipkow |
added zdvd_iff_zmod_eq_0
|
changeset |
files
|