Wed, 20 Nov 2002 10:43:20 +0100 paulson textual tweak
Tue, 19 Nov 2002 10:41:20 +0100 paulson stylistic tweaks
Mon, 18 Nov 2002 14:51:44 +0100 nipkow beautification
Sun, 17 Nov 2002 23:43:53 +0100 berghofe Fixed small bug that caused some definitions to be "forgotten".
Sat, 16 Nov 2002 23:01:59 +0100 kleing beautified "match"
Sat, 16 Nov 2002 22:54:39 +0100 kleing beautified "match"
Fri, 15 Nov 2002 18:02:25 +0100 nipkow added zdvd_iff_zmod_eq_0
Wed, 13 Nov 2002 15:36:36 +0100 berghofe Improved function decompose.
Wed, 13 Nov 2002 15:36:06 +0100 berghofe - exported functions etype_of and mk_typ
Wed, 13 Nov 2002 15:35:15 +0100 berghofe Fixed name clash problem in forall_elim_var.
Wed, 13 Nov 2002 15:34:35 +0100 berghofe Added simple_prove_goal_cterm.
Wed, 13 Nov 2002 15:34:01 +0100 berghofe Removed (now unneeded) declarations of realizers for bar induction.
Wed, 13 Nov 2002 15:32:41 +0100 berghofe New package for constructing realizers for introduction and elimination
Wed, 13 Nov 2002 15:31:14 +0100 berghofe - No longer applies norm_hhf_rule
Wed, 13 Nov 2002 15:28:41 +0100 berghofe prove_goal' -> Goal.simple_prove_goal_cterm
Wed, 13 Nov 2002 15:27:27 +0100 berghofe name_of_type now replaces non-identifiers by dummy names.
Wed, 13 Nov 2002 15:26:19 +0100 berghofe Added inductive_realizer.
Wed, 13 Nov 2002 15:25:17 +0100 berghofe Added InductiveRealizer package.
Wed, 13 Nov 2002 15:24:42 +0100 berghofe Transitive closure is now defined inductively as well.
Sat, 09 Nov 2002 00:12:25 +0100 kleing Hoare.ML -> hoare.ML
Fri, 08 Nov 2002 10:34:40 +0100 paulson Polishing.
Fri, 08 Nov 2002 10:28:29 +0100 paulson generalized wf_on_unit to wf_on_any_0
Thu, 07 Nov 2002 12:35:34 +0100 nipkow added raw proof blocks
Thu, 07 Nov 2002 09:26:44 +0100 nipkow small improvements
Thu, 07 Nov 2002 09:08:25 +0100 nipkow added show_main_goal
Wed, 06 Nov 2002 14:02:18 +0100 nipkow Hoare.ML -> hoare.ML
Wed, 06 Nov 2002 14:01:38 +0100 nipkow a new pointer example and some syntactic sugar
Tue, 05 Nov 2002 15:59:17 +0100 kleing two new Bali files
Tue, 05 Nov 2002 15:51:18 +0100 paulson new operator transrec3
Mon, 04 Nov 2002 14:17:00 +0100 berghofe Removed obsolete section about reordering assumptions.
Fri, 01 Nov 2002 17:44:26 +0100 paulson proof streamlining
Fri, 01 Nov 2002 17:43:54 +0100 paulson tidy
Fri, 01 Nov 2002 13:16:28 +0100 schirmer Inserted some extra paragraphs in large proofs to make tex run...
Fri, 01 Nov 2002 10:35:50 +0100 kleing fixed "latex capacity exceeded"
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.
Wed, 30 Oct 2002 12:44:18 +0100 paulson simpler separation/replacement proofs
Wed, 30 Oct 2002 12:18:23 +0100 nipkow modified msg
Tue, 29 Oct 2002 11:32:52 +0100 nipkow added induction thms
Mon, 28 Oct 2002 17:56:00 +0100 nipkow moved fac example
Mon, 28 Oct 2002 14:30:37 +0100 nipkow *** empty log message ***
Mon, 28 Oct 2002 14:29:51 +0100 nipkow conversion ML -> thy
Sun, 27 Oct 2002 23:34:02 +0100 kleing simplified lemma correct_frames_newref
Sat, 26 Oct 2002 13:05:27 +0200 isatest switched to atbroy51, removed markus from email list
Fri, 25 Oct 2002 10:47:47 +0200 kleing fixed latex output
Thu, 24 Oct 2002 12:08:33 +0200 kleing changes for cleanup in JVM
Thu, 24 Oct 2002 12:07:31 +0200 kleing cleanup, beautified
Thu, 24 Oct 2002 12:06:43 +0200 kleing fixed latex error
Thu, 24 Oct 2002 07:23:46 +0200 nipkow ASIN -> SET
Wed, 23 Oct 2002 16:10:42 +0200 streckem *** empty log message ***
Wed, 23 Oct 2002 16:10:02 +0200 streckem First checkin of compiler
Wed, 23 Oct 2002 16:09:02 +0200 streckem Added compiler
Mon, 21 Oct 2002 17:23:23 +0200 berghofe Eta contraction is now switched off when printing extracted program.
Mon, 21 Oct 2002 17:20:29 +0200 berghofe Fixed problem with theorems containing TFrees.
Mon, 21 Oct 2002 17:19:51 +0200 berghofe - reconstruct_proof no longer relies on TypeInfer.infer_types
Mon, 21 Oct 2002 17:17:40 +0200 berghofe Removed Logic.skip_flexpairs.
Mon, 21 Oct 2002 17:16:24 +0200 berghofe Replaced variantlist (quadratic) by gen_names (linear).
Mon, 21 Oct 2002 17:15:40 +0200 berghofe Removed add_env because Vartab.map was too slow for large environments.
Mon, 21 Oct 2002 17:14:19 +0200 berghofe - removed flexpair
Mon, 21 Oct 2002 17:12:44 +0200 berghofe No more explicit manipulation of flex-flex constraints in metahyps_aux_tac.
Mon, 21 Oct 2002 17:11:29 +0200 berghofe Removed flexpair_def.
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip