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