berghofe [Wed, 13 Nov 2002 15:25:17 +0100] rev 13705
Added InductiveRealizer package.
berghofe [Wed, 13 Nov 2002 15:24:42 +0100] rev 13704
Transitive closure is now defined inductively as well.
kleing [Sat, 09 Nov 2002 00:12:25 +0100] rev 13703
Hoare.ML -> hoare.ML
paulson [Fri, 08 Nov 2002 10:34:40 +0100] rev 13702
Polishing.
lambda_abs2 doesn't need an instance of replacement
various renamings & restructurings
paulson [Fri, 08 Nov 2002 10:28:29 +0100] rev 13701
generalized wf_on_unit to wf_on_any_0
nipkow [Thu, 07 Nov 2002 12:35:34 +0100] rev 13700
added raw proof blocks
nipkow [Thu, 07 Nov 2002 09:26:44 +0100] rev 13699
small improvements
nipkow [Thu, 07 Nov 2002 09:08:25 +0100] rev 13698
added show_main_goal
nipkow [Wed, 06 Nov 2002 14:02:18 +0100] rev 13697
Hoare.ML -> hoare.ML
nipkow [Wed, 06 Nov 2002 14:01:38 +0100] rev 13696
a new pointer example and some syntactic sugar
kleing [Tue, 05 Nov 2002 15:59:17 +0100] rev 13695
two new Bali files
paulson [Tue, 05 Nov 2002 15:51:18 +0100] rev 13694
new operator transrec3
berghofe [Mon, 04 Nov 2002 14:17:00 +0100] rev 13693
Removed obsolete section about reordering assumptions.
paulson [Fri, 01 Nov 2002 17:44:26 +0100] rev 13692
proof streamlining
paulson [Fri, 01 Nov 2002 17:43:54 +0100] rev 13691
tidy
schirmer [Fri, 01 Nov 2002 13:16:28 +0100] rev 13690
Inserted some extra paragraphs in large proofs to make tex run...
kleing [Fri, 01 Nov 2002 10:35:50 +0100] rev 13689
fixed "latex capacity exceeded"
schirmer [Thu, 31 Oct 2002 18:27:10 +0100] rev 13688
"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.
paulson [Wed, 30 Oct 2002 12:44:18 +0100] rev 13687
simpler separation/replacement proofs
nipkow [Wed, 30 Oct 2002 12:18:23 +0100] rev 13686
modified msg
nipkow [Tue, 29 Oct 2002 11:32:52 +0100] rev 13685
added induction thms
nipkow [Mon, 28 Oct 2002 17:56:00 +0100] rev 13684
moved fac example
nipkow [Mon, 28 Oct 2002 14:30:37 +0100] rev 13683
*** empty log message ***
nipkow [Mon, 28 Oct 2002 14:29:51 +0100] rev 13682
conversion ML -> thy
kleing [Sun, 27 Oct 2002 23:34:02 +0100] rev 13681
simplified lemma correct_frames_newref
isatest [Sat, 26 Oct 2002 13:05:27 +0200] rev 13680
switched to atbroy51, removed markus from email list
kleing [Fri, 25 Oct 2002 10:47:47 +0200] rev 13679
fixed latex output
kleing [Thu, 24 Oct 2002 12:08:33 +0200] rev 13678
changes for cleanup in JVM
kleing [Thu, 24 Oct 2002 12:07:31 +0200] rev 13677
cleanup, beautified
kleing [Thu, 24 Oct 2002 12:06:43 +0200] rev 13676
fixed latex error
nipkow [Thu, 24 Oct 2002 07:23:46 +0200] rev 13675
ASIN -> SET
streckem [Wed, 23 Oct 2002 16:10:42 +0200] rev 13674
*** empty log message ***
streckem [Wed, 23 Oct 2002 16:10:02 +0200] rev 13673
First checkin of compiler
streckem [Wed, 23 Oct 2002 16:09:02 +0200] rev 13672
Added compiler
berghofe [Mon, 21 Oct 2002 17:23:23 +0200] rev 13671
Eta contraction is now switched off when printing extracted program.
berghofe [Mon, 21 Oct 2002 17:20:29 +0200] rev 13670
Fixed problem with theorems containing TFrees.
berghofe [Mon, 21 Oct 2002 17:19:51 +0200] rev 13669
- reconstruct_proof no longer relies on TypeInfer.infer_types
- fixed problem with theorems containing TFrees
berghofe [Mon, 21 Oct 2002 17:17:40 +0200] rev 13668
Removed Logic.skip_flexpairs.
berghofe [Mon, 21 Oct 2002 17:16:24 +0200] rev 13667
Replaced variantlist (quadratic) by gen_names (linear).
berghofe [Mon, 21 Oct 2002 17:15:40 +0200] rev 13666
Removed add_env because Vartab.map was too slow for large environments.
berghofe [Mon, 21 Oct 2002 17:14:19 +0200] rev 13665
- removed flexpair
- added maxidx_of_terms
- tuned lambda: now also abstracts over Vars
berghofe [Mon, 21 Oct 2002 17:12:44 +0200] rev 13664
No more explicit manipulation of flex-flex constraints in metahyps_aux_tac.
berghofe [Mon, 21 Oct 2002 17:11:29 +0200] rev 13663
Removed flexpair_def.
berghofe [Mon, 21 Oct 2002 17:11:06 +0200] rev 13662
Removed Logic.strip_flexpairs.
berghofe [Mon, 21 Oct 2002 17:09:31 +0200] rev 13661
No more explicit manipulation of flex-flex constraints in goals_conv.
berghofe [Mon, 21 Oct 2002 17:07:58 +0200] rev 13660
Changed type of Logic.strip_horn.
berghofe [Mon, 21 Oct 2002 17:07:27 +0200] rev 13659
Removed obsolete functions dealing with flex-flex constraints.
berghofe [Mon, 21 Oct 2002 17:04:47 +0200] rev 13658
Changed handling of flex-flex constraints: now stored in separate
tpairs field of theorem record.
berghofe [Mon, 21 Oct 2002 17:00:45 +0200] rev 13657
Now applies standard' to "unfold" theorem (due to flex-flex constraints).
berghofe [Mon, 21 Oct 2002 16:57:39 +0200] rev 13656
Changed type of Logic.strip_horn.
paulson [Fri, 18 Oct 2002 17:50:13 +0200] rev 13655
Tidying up. New primitives is_iterates and is_iterates_fm.
nipkow [Fri, 18 Oct 2002 09:53:18 +0200] rev 13654
Mod due to: Added a few thms about UN/INT/{}/UNIV
nipkow [Fri, 18 Oct 2002 09:53:02 +0200] rev 13653
Added a few thms about UN/INT/{}/UNIV
paulson [Thu, 17 Oct 2002 10:56:00 +0200] rev 13652
fixed comments and types
paulson [Thu, 17 Oct 2002 10:54:11 +0200] rev 13651
Cosmetic changes suggested by writing the paper. Deleted some
redundant arity proofs
paulson [Thu, 17 Oct 2002 10:52:59 +0200] rev 13650
fixing the cut_tac method to work when there are no instantiations and the
supplied theorems have premises