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.
Mon, 21 Oct 2002 17:11:06 +0200 berghofe Removed Logic.strip_flexpairs.
Mon, 21 Oct 2002 17:09:31 +0200 berghofe No more explicit manipulation of flex-flex constraints in goals_conv.
Mon, 21 Oct 2002 17:07:58 +0200 berghofe Changed type of Logic.strip_horn.
Mon, 21 Oct 2002 17:07:27 +0200 berghofe Removed obsolete functions dealing with flex-flex constraints.
Mon, 21 Oct 2002 17:04:47 +0200 berghofe Changed handling of flex-flex constraints: now stored in separate
Mon, 21 Oct 2002 17:00:45 +0200 berghofe Now applies standard' to "unfold" theorem (due to flex-flex constraints).
Mon, 21 Oct 2002 16:57:39 +0200 berghofe Changed type of Logic.strip_horn.
Fri, 18 Oct 2002 17:50:13 +0200 paulson Tidying up. New primitives is_iterates and is_iterates_fm.
Fri, 18 Oct 2002 09:53:18 +0200 nipkow Mod due to: Added a few thms about UN/INT/{}/UNIV
Fri, 18 Oct 2002 09:53:02 +0200 nipkow Added a few thms about UN/INT/{}/UNIV
Thu, 17 Oct 2002 10:56:00 +0200 paulson fixed comments and types
Thu, 17 Oct 2002 10:54:11 +0200 paulson Cosmetic changes suggested by writing the paper. Deleted some
Thu, 17 Oct 2002 10:52:59 +0200 paulson fixing the cut_tac method to work when there are no instantiations and the
Tue, 15 Oct 2002 15:37:57 +0200 kleing alternative syntax
Mon, 14 Oct 2002 13:35:17 +0200 nipkow *** empty log message ***
Mon, 14 Oct 2002 11:32:00 +0200 paulson tidying and reorganization
Mon, 14 Oct 2002 10:44:32 +0200 nipkow Ported find_intro/elim to Isar.
Fri, 11 Oct 2002 12:47:52 +0200 berghofe norm_typ -> Envir.norm_type
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip