| 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
|
| Wed, 13 Nov 2002 15:36:36 +0100 |
berghofe |
Improved function decompose.
|
changeset |
files
|
| Wed, 13 Nov 2002 15:36:06 +0100 |
berghofe |
- exported functions etype_of and mk_typ
|
changeset |
files
|
| Wed, 13 Nov 2002 15:35:15 +0100 |
berghofe |
Fixed name clash problem in forall_elim_var.
|
changeset |
files
|
| Wed, 13 Nov 2002 15:34:35 +0100 |
berghofe |
Added simple_prove_goal_cterm.
|
changeset |
files
|
| Wed, 13 Nov 2002 15:34:01 +0100 |
berghofe |
Removed (now unneeded) declarations of realizers for bar induction.
|
changeset |
files
|
| Wed, 13 Nov 2002 15:32:41 +0100 |
berghofe |
New package for constructing realizers for introduction and elimination
|
changeset |
files
|
| Wed, 13 Nov 2002 15:31:14 +0100 |
berghofe |
- No longer applies norm_hhf_rule
|
changeset |
files
|