| Wed, 30 Oct 2002 12:44:18 +0100 |
paulson |
simpler separation/replacement proofs
|
changeset |
files
|
| Wed, 30 Oct 2002 12:18:23 +0100 |
nipkow |
modified msg
|
changeset |
files
|
| Tue, 29 Oct 2002 11:32:52 +0100 |
nipkow |
added induction thms
|
changeset |
files
|
| Mon, 28 Oct 2002 17:56:00 +0100 |
nipkow |
moved fac example
|
changeset |
files
|
| Mon, 28 Oct 2002 14:30:37 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Mon, 28 Oct 2002 14:29:51 +0100 |
nipkow |
conversion ML -> thy
|
changeset |
files
|
| Sun, 27 Oct 2002 23:34:02 +0100 |
kleing |
simplified lemma correct_frames_newref
|
changeset |
files
|
| Sat, 26 Oct 2002 13:05:27 +0200 |
isatest |
switched to atbroy51, removed markus from email list
|
changeset |
files
|
| Fri, 25 Oct 2002 10:47:47 +0200 |
kleing |
fixed latex output
|
changeset |
files
|
| Thu, 24 Oct 2002 12:08:33 +0200 |
kleing |
changes for cleanup in JVM
|
changeset |
files
|
| Thu, 24 Oct 2002 12:07:31 +0200 |
kleing |
cleanup, beautified
|
changeset |
files
|
| Thu, 24 Oct 2002 12:06:43 +0200 |
kleing |
fixed latex error
|
changeset |
files
|
| Thu, 24 Oct 2002 07:23:46 +0200 |
nipkow |
ASIN -> SET
|
changeset |
files
|
| Wed, 23 Oct 2002 16:10:42 +0200 |
streckem |
*** empty log message ***
|
changeset |
files
|
| Wed, 23 Oct 2002 16:10:02 +0200 |
streckem |
First checkin of compiler
|
changeset |
files
|
| Wed, 23 Oct 2002 16:09:02 +0200 |
streckem |
Added compiler
|
changeset |
files
|
| Mon, 21 Oct 2002 17:23:23 +0200 |
berghofe |
Eta contraction is now switched off when printing extracted program.
|
changeset |
files
|
| Mon, 21 Oct 2002 17:20:29 +0200 |
berghofe |
Fixed problem with theorems containing TFrees.
|
changeset |
files
|
| Mon, 21 Oct 2002 17:19:51 +0200 |
berghofe |
- reconstruct_proof no longer relies on TypeInfer.infer_types
|
changeset |
files
|
| Mon, 21 Oct 2002 17:17:40 +0200 |
berghofe |
Removed Logic.skip_flexpairs.
|
changeset |
files
|
| Mon, 21 Oct 2002 17:16:24 +0200 |
berghofe |
Replaced variantlist (quadratic) by gen_names (linear).
|
changeset |
files
|
| Mon, 21 Oct 2002 17:15:40 +0200 |
berghofe |
Removed add_env because Vartab.map was too slow for large environments.
|
changeset |
files
|
| Mon, 21 Oct 2002 17:14:19 +0200 |
berghofe |
- removed flexpair
|
changeset |
files
|
| Mon, 21 Oct 2002 17:12:44 +0200 |
berghofe |
No more explicit manipulation of flex-flex constraints in metahyps_aux_tac.
|
changeset |
files
|
| Mon, 21 Oct 2002 17:11:29 +0200 |
berghofe |
Removed flexpair_def.
|
changeset |
files
|
| Mon, 21 Oct 2002 17:11:06 +0200 |
berghofe |
Removed Logic.strip_flexpairs.
|
changeset |
files
|
| Mon, 21 Oct 2002 17:09:31 +0200 |
berghofe |
No more explicit manipulation of flex-flex constraints in goals_conv.
|
changeset |
files
|
| Mon, 21 Oct 2002 17:07:58 +0200 |
berghofe |
Changed type of Logic.strip_horn.
|
changeset |
files
|
| Mon, 21 Oct 2002 17:07:27 +0200 |
berghofe |
Removed obsolete functions dealing with flex-flex constraints.
|
changeset |
files
|
| Mon, 21 Oct 2002 17:04:47 +0200 |
berghofe |
Changed handling of flex-flex constraints: now stored in separate
|
changeset |
files
|