| 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
|
| Wed, 13 Nov 2002 15:28:41 +0100 |
berghofe |
prove_goal' -> Goal.simple_prove_goal_cterm
|
changeset |
files
|
| Wed, 13 Nov 2002 15:27:27 +0100 |
berghofe |
name_of_type now replaces non-identifiers by dummy names.
|
changeset |
files
|
| Wed, 13 Nov 2002 15:26:19 +0100 |
berghofe |
Added inductive_realizer.
|
changeset |
files
|
| Wed, 13 Nov 2002 15:25:17 +0100 |
berghofe |
Added InductiveRealizer package.
|
changeset |
files
|
| Wed, 13 Nov 2002 15:24:42 +0100 |
berghofe |
Transitive closure is now defined inductively as well.
|
changeset |
files
|
| Sat, 09 Nov 2002 00:12:25 +0100 |
kleing |
Hoare.ML -> hoare.ML
|
changeset |
files
|
| Fri, 08 Nov 2002 10:34:40 +0100 |
paulson |
Polishing.
|
changeset |
files
|
| Fri, 08 Nov 2002 10:28:29 +0100 |
paulson |
generalized wf_on_unit to wf_on_any_0
|
changeset |
files
|
| Thu, 07 Nov 2002 12:35:34 +0100 |
nipkow |
added raw proof blocks
|
changeset |
files
|
| Thu, 07 Nov 2002 09:26:44 +0100 |
nipkow |
small improvements
|
changeset |
files
|
| Thu, 07 Nov 2002 09:08:25 +0100 |
nipkow |
added show_main_goal
|
changeset |
files
|
| Wed, 06 Nov 2002 14:02:18 +0100 |
nipkow |
Hoare.ML -> hoare.ML
|
changeset |
files
|
| Wed, 06 Nov 2002 14:01:38 +0100 |
nipkow |
a new pointer example and some syntactic sugar
|
changeset |
files
|
| Tue, 05 Nov 2002 15:59:17 +0100 |
kleing |
two new Bali files
|
changeset |
files
|
| Tue, 05 Nov 2002 15:51:18 +0100 |
paulson |
new operator transrec3
|
changeset |
files
|
| Mon, 04 Nov 2002 14:17:00 +0100 |
berghofe |
Removed obsolete section about reordering assumptions.
|
changeset |
files
|
| Fri, 01 Nov 2002 17:44:26 +0100 |
paulson |
proof streamlining
|
changeset |
files
|
| Fri, 01 Nov 2002 17:43:54 +0100 |
paulson |
tidy
|
changeset |
files
|
| Fri, 01 Nov 2002 13:16:28 +0100 |
schirmer |
Inserted some extra paragraphs in large proofs to make tex run...
|
changeset |
files
|
| Fri, 01 Nov 2002 10:35:50 +0100 |
kleing |
fixed "latex capacity exceeded"
|
changeset |
files
|
| 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
|