oheimb [Fri, 13 Dec 2002 18:14:25 +0100] rev 13752
cent/currency: changed from wasysym to textcomp because of PDF problems
paulson [Fri, 13 Dec 2002 16:49:08 +0100] rev 13751
trace_unify_fail
paulson [Fri, 13 Dec 2002 16:48:20 +0100] rev 13750
integer induction rules
berghofe [Fri, 13 Dec 2002 14:20:47 +0100] rev 13749
size_of_proof no longer includes size_of_term
paulson [Fri, 13 Dec 2002 13:47:13 +0100] rev 13748
deleted redundant line
paulson [Thu, 12 Dec 2002 11:38:18 +0100] rev 13747
Better treatment of equality in premises of inductive definitions. Less
backtracking.
ballarin [Thu, 12 Dec 2002 11:33:48 +0100] rev 13746
Fixed error that affected document preperation.
ballarin [Wed, 11 Dec 2002 10:12:48 +0100] rev 13745
HOL/GroupTheory/Summation.thy added: summation operator for abelian groups.
berghofe [Tue, 10 Dec 2002 10:40:32 +0100] rev 13744
Added size_of_proof.
ballarin [Mon, 09 Dec 2002 10:38:56 +0100] rev 13743
Fixed bug in simpdata.ML that prevented the use of congruence rules from a
locale. (mk_meta_cong did wrongly convert metahyps to hyps)
oheimb [Fri, 06 Dec 2002 15:16:30 +0100] rev 13742
corrected swallowing of newlines after end-of-ignore
nipkow [Fri, 06 Dec 2002 11:09:02 +0100] rev 13741
*** empty log message ***
kleing [Thu, 05 Dec 2002 18:44:16 +0100] rev 13740
for dvi target
kleing [Thu, 05 Dec 2002 17:12:07 +0100] rev 13739
exercise collection
ballarin [Fri, 29 Nov 2002 14:26:55 +0100] rev 13738
Incompatibility with SML/NJ fixed.
nipkow [Fri, 29 Nov 2002 09:48:28 +0100] rev 13737
added a few lemmas
ballarin [Thu, 28 Nov 2002 15:44:34 +0100] rev 13736
Transitivity reasoner renamed to linorder.ML. README updated.
ballarin [Thu, 28 Nov 2002 10:50:42 +0100] rev 13735
HOL-Algebra partially ported to Isar.
berghofe [Wed, 27 Nov 2002 17:25:41 +0100] rev 13734
prop_of now returns proposition in beta-eta normal form.
berghofe [Wed, 27 Nov 2002 17:25:04 +0100] rev 13733
- tuned beta_eta_convert
- returned theorem is now in beta-eta normal form
berghofe [Wed, 27 Nov 2002 17:23:19 +0100] rev 13732
Correctness proofs are now modular, too.
berghofe [Wed, 27 Nov 2002 17:22:18 +0100] rev 13731
Parameters in definitions are now renamed to avoid clashes with
reserved ML keywords.
berghofe [Wed, 27 Nov 2002 17:20:49 +0100] rev 13730
default_output now escapes \'s more carefully.
berghofe [Wed, 27 Nov 2002 17:17:53 +0100] rev 13729
Added XML parser (useful for parsing PGIP / PGML).
berghofe [Wed, 27 Nov 2002 17:16:47 +0100] rev 13728
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe [Wed, 27 Nov 2002 17:11:38 +0100] rev 13727
Fixed bug in consts_code section.
berghofe [Wed, 27 Nov 2002 17:07:05 +0100] rev 13726
Replaced some blasts by rules.
berghofe [Wed, 27 Nov 2002 17:06:47 +0100] rev 13725
Changed format of realizers / correctness proofs.
nipkow [Mon, 25 Nov 2002 20:32:29 +0100] rev 13724
renamed a few constants
nipkow [Thu, 21 Nov 2002 17:40:11 +0100] rev 13723
*** empty log message ***
paulson [Wed, 20 Nov 2002 10:43:20 +0100] rev 13722
textual tweak
paulson [Tue, 19 Nov 2002 10:41:20 +0100] rev 13721
stylistic tweaks
nipkow [Mon, 18 Nov 2002 14:51:44 +0100] rev 13720
beautification
berghofe [Sun, 17 Nov 2002 23:43:53 +0100] rev 13719
Fixed small bug that caused some definitions to be "forgotten".
kleing [Sat, 16 Nov 2002 23:01:59 +0100] rev 13718
beautified "match"
kleing [Sat, 16 Nov 2002 22:54:39 +0100] rev 13717
beautified "match"
nipkow [Fri, 15 Nov 2002 18:02:25 +0100] rev 13716
added zdvd_iff_zmod_eq_0
berghofe [Wed, 13 Nov 2002 15:36:36 +0100] rev 13715
Improved function decompose.
berghofe [Wed, 13 Nov 2002 15:36:06 +0100] rev 13714
- exported functions etype_of and mk_typ
- new function realizes_of
berghofe [Wed, 13 Nov 2002 15:35:15 +0100] rev 13713
Fixed name clash problem in forall_elim_var.
berghofe [Wed, 13 Nov 2002 15:34:35 +0100] rev 13712
Added simple_prove_goal_cterm.
berghofe [Wed, 13 Nov 2002 15:34:01 +0100] rev 13711
Removed (now unneeded) declarations of realizers for bar induction.
berghofe [Wed, 13 Nov 2002 15:32:41 +0100] rev 13710
New package for constructing realizers for introduction and elimination
rules of inductive predicates.
berghofe [Wed, 13 Nov 2002 15:31:14 +0100] rev 13709
- No longer applies norm_hhf_rule
- intrs field now contains theorems with names specified by user
berghofe [Wed, 13 Nov 2002 15:28:41 +0100] rev 13708
prove_goal' -> Goal.simple_prove_goal_cterm
berghofe [Wed, 13 Nov 2002 15:27:27 +0100] rev 13707
name_of_type now replaces non-identifiers by dummy names.
berghofe [Wed, 13 Nov 2002 15:26:19 +0100] rev 13706
Added inductive_realizer.
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).