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