| Thu, 31 Oct 2002 18:27:10 +0100 |
schirmer |
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
|
changeset |
files
|
| 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
|
| Mon, 21 Oct 2002 17:00:45 +0200 |
berghofe |
Now applies standard' to "unfold" theorem (due to flex-flex constraints).
|
changeset |
files
|
| Mon, 21 Oct 2002 16:57:39 +0200 |
berghofe |
Changed type of Logic.strip_horn.
|
changeset |
files
|
| Fri, 18 Oct 2002 17:50:13 +0200 |
paulson |
Tidying up. New primitives is_iterates and is_iterates_fm.
|
changeset |
files
|
| Fri, 18 Oct 2002 09:53:18 +0200 |
nipkow |
Mod due to: Added a few thms about UN/INT/{}/UNIV
|
changeset |
files
|
| Fri, 18 Oct 2002 09:53:02 +0200 |
nipkow |
Added a few thms about UN/INT/{}/UNIV
|
changeset |
files
|
| Thu, 17 Oct 2002 10:56:00 +0200 |
paulson |
fixed comments and types
|
changeset |
files
|
| Thu, 17 Oct 2002 10:54:11 +0200 |
paulson |
Cosmetic changes suggested by writing the paper. Deleted some
|
changeset |
files
|
| Thu, 17 Oct 2002 10:52:59 +0200 |
paulson |
fixing the cut_tac method to work when there are no instantiations and the
|
changeset |
files
|
| Tue, 15 Oct 2002 15:37:57 +0200 |
kleing |
alternative syntax
|
changeset |
files
|
| Mon, 14 Oct 2002 13:35:17 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Mon, 14 Oct 2002 11:32:00 +0200 |
paulson |
tidying and reorganization
|
changeset |
files
|
| Mon, 14 Oct 2002 10:44:32 +0200 |
nipkow |
Ported find_intro/elim to Isar.
|
changeset |
files
|
| Fri, 11 Oct 2002 12:47:52 +0200 |
berghofe |
norm_typ -> Envir.norm_type
|
changeset |
files
|
| Thu, 10 Oct 2002 19:24:34 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Thu, 10 Oct 2002 19:03:37 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Thu, 10 Oct 2002 19:02:23 +0200 |
nipkow |
added failure trace information to pattern unification
|
changeset |
files
|
| Thu, 10 Oct 2002 14:26:50 +0200 |
berghofe |
Reimplemented parts of datatype package dealing with datatypes involving
|
changeset |
files
|
| Thu, 10 Oct 2002 14:23:47 +0200 |
berghofe |
Added list_all.
|
changeset |
files
|
| Thu, 10 Oct 2002 14:23:19 +0200 |
berghofe |
Removed obsolete function "fun_rel_comp".
|
changeset |
files
|
| Thu, 10 Oct 2002 14:21:49 +0200 |
berghofe |
Added choice_eq.
|
changeset |
files
|
| Thu, 10 Oct 2002 14:21:20 +0200 |
berghofe |
- Added range_ex1_eq
|
changeset |
files
|
| Thu, 10 Oct 2002 14:19:17 +0200 |
berghofe |
Removed obsolete function "Funs".
|
changeset |
files
|
| Thu, 10 Oct 2002 14:18:01 +0200 |
berghofe |
Added functions Suml and Sumr which are useful for constructing
|
changeset |
files
|
| Wed, 09 Oct 2002 11:07:13 +0200 |
paulson |
Re-organization of Constructible theories
|
changeset |
files
|
| Tue, 08 Oct 2002 14:09:18 +0200 |
kleing |
type safety with defensive machine
|
changeset |
files
|
| Tue, 08 Oct 2002 14:08:50 +0200 |
kleing |
defensive machine
|
changeset |
files
|
| Tue, 08 Oct 2002 10:49:19 +0200 |
kleing |
defensive machine without obj init and jsr
|
changeset |
files
|
| Tue, 08 Oct 2002 08:20:17 +0200 |
nipkow |
Got rid of rotates because of new simplifier
|
changeset |
files
|
| Mon, 07 Oct 2002 19:01:51 +0200 |
nipkow |
take/drop -> splitAt
|
changeset |
files
|