| Thu, 05 Dec 2002 17:12:07 +0100 |
kleing |
exercise collection
|
changeset |
files
|
| Fri, 29 Nov 2002 14:26:55 +0100 |
ballarin |
Incompatibility with SML/NJ fixed.
|
changeset |
files
|
| Fri, 29 Nov 2002 09:48:28 +0100 |
nipkow |
added a few lemmas
|
changeset |
files
|
| Thu, 28 Nov 2002 15:44:34 +0100 |
ballarin |
Transitivity reasoner renamed to linorder.ML. README updated.
|
changeset |
files
|
| Thu, 28 Nov 2002 10:50:42 +0100 |
ballarin |
HOL-Algebra partially ported to Isar.
|
changeset |
files
|
| Wed, 27 Nov 2002 17:25:41 +0100 |
berghofe |
prop_of now returns proposition in beta-eta normal form.
|
changeset |
files
|
| Wed, 27 Nov 2002 17:25:04 +0100 |
berghofe |
- tuned beta_eta_convert
|
changeset |
files
|
| Wed, 27 Nov 2002 17:23:19 +0100 |
berghofe |
Correctness proofs are now modular, too.
|
changeset |
files
|
| Wed, 27 Nov 2002 17:22:18 +0100 |
berghofe |
Parameters in definitions are now renamed to avoid clashes with
|
changeset |
files
|
| Wed, 27 Nov 2002 17:20:49 +0100 |
berghofe |
default_output now escapes \'s more carefully.
|
changeset |
files
|
| Wed, 27 Nov 2002 17:17:53 +0100 |
berghofe |
Added XML parser (useful for parsing PGIP / PGML).
|
changeset |
files
|
| Wed, 27 Nov 2002 17:16:47 +0100 |
berghofe |
Added some functions for processing PGIP (thanks to David Aspinall).
|
changeset |
files
|
| Wed, 27 Nov 2002 17:11:38 +0100 |
berghofe |
Fixed bug in consts_code section.
|
changeset |
files
|
| Wed, 27 Nov 2002 17:07:05 +0100 |
berghofe |
Replaced some blasts by rules.
|
changeset |
files
|
| Wed, 27 Nov 2002 17:06:47 +0100 |
berghofe |
Changed format of realizers / correctness proofs.
|
changeset |
files
|
| Mon, 25 Nov 2002 20:32:29 +0100 |
nipkow |
renamed a few constants
|
changeset |
files
|
| Thu, 21 Nov 2002 17:40:11 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 20 Nov 2002 10:43:20 +0100 |
paulson |
textual tweak
|
changeset |
files
|
| Tue, 19 Nov 2002 10:41:20 +0100 |
paulson |
stylistic tweaks
|
changeset |
files
|
| Mon, 18 Nov 2002 14:51:44 +0100 |
nipkow |
beautification
|
changeset |
files
|
| Sun, 17 Nov 2002 23:43:53 +0100 |
berghofe |
Fixed small bug that caused some definitions to be "forgotten".
|
changeset |
files
|
| Sat, 16 Nov 2002 23:01:59 +0100 |
kleing |
beautified "match"
|
changeset |
files
|
| Sat, 16 Nov 2002 22:54:39 +0100 |
kleing |
beautified "match"
|
changeset |
files
|
| Fri, 15 Nov 2002 18:02:25 +0100 |
nipkow |
added zdvd_iff_zmod_eq_0
|
changeset |
files
|
| Wed, 13 Nov 2002 15:36:36 +0100 |
berghofe |
Improved function decompose.
|
changeset |
files
|
| Wed, 13 Nov 2002 15:36:06 +0100 |
berghofe |
- exported functions etype_of and mk_typ
|
changeset |
files
|
| Wed, 13 Nov 2002 15:35:15 +0100 |
berghofe |
Fixed name clash problem in forall_elim_var.
|
changeset |
files
|
| Wed, 13 Nov 2002 15:34:35 +0100 |
berghofe |
Added simple_prove_goal_cterm.
|
changeset |
files
|
| Wed, 13 Nov 2002 15:34:01 +0100 |
berghofe |
Removed (now unneeded) declarations of realizers for bar induction.
|
changeset |
files
|
| Wed, 13 Nov 2002 15:32:41 +0100 |
berghofe |
New package for constructing realizers for introduction and elimination
|
changeset |
files
|
| Wed, 13 Nov 2002 15:31:14 +0100 |
berghofe |
- No longer applies norm_hhf_rule
|
changeset |
files
|
| Wed, 13 Nov 2002 15:28:41 +0100 |
berghofe |
prove_goal' -> Goal.simple_prove_goal_cterm
|
changeset |
files
|
| Wed, 13 Nov 2002 15:27:27 +0100 |
berghofe |
name_of_type now replaces non-identifiers by dummy names.
|
changeset |
files
|
| Wed, 13 Nov 2002 15:26:19 +0100 |
berghofe |
Added inductive_realizer.
|
changeset |
files
|
| Wed, 13 Nov 2002 15:25:17 +0100 |
berghofe |
Added InductiveRealizer package.
|
changeset |
files
|
| Wed, 13 Nov 2002 15:24:42 +0100 |
berghofe |
Transitive closure is now defined inductively as well.
|
changeset |
files
|
| Sat, 09 Nov 2002 00:12:25 +0100 |
kleing |
Hoare.ML -> hoare.ML
|
changeset |
files
|
| Fri, 08 Nov 2002 10:34:40 +0100 |
paulson |
Polishing.
|
changeset |
files
|
| Fri, 08 Nov 2002 10:28:29 +0100 |
paulson |
generalized wf_on_unit to wf_on_any_0
|
changeset |
files
|
| Thu, 07 Nov 2002 12:35:34 +0100 |
nipkow |
added raw proof blocks
|
changeset |
files
|
| Thu, 07 Nov 2002 09:26:44 +0100 |
nipkow |
small improvements
|
changeset |
files
|
| Thu, 07 Nov 2002 09:08:25 +0100 |
nipkow |
added show_main_goal
|
changeset |
files
|
| Wed, 06 Nov 2002 14:02:18 +0100 |
nipkow |
Hoare.ML -> hoare.ML
|
changeset |
files
|
| Wed, 06 Nov 2002 14:01:38 +0100 |
nipkow |
a new pointer example and some syntactic sugar
|
changeset |
files
|
| Tue, 05 Nov 2002 15:59:17 +0100 |
kleing |
two new Bali files
|
changeset |
files
|
| Tue, 05 Nov 2002 15:51:18 +0100 |
paulson |
new operator transrec3
|
changeset |
files
|
| Mon, 04 Nov 2002 14:17:00 +0100 |
berghofe |
Removed obsolete section about reordering assumptions.
|
changeset |
files
|
| Fri, 01 Nov 2002 17:44:26 +0100 |
paulson |
proof streamlining
|
changeset |
files
|
| Fri, 01 Nov 2002 17:43:54 +0100 |
paulson |
tidy
|
changeset |
files
|
| Fri, 01 Nov 2002 13:16:28 +0100 |
schirmer |
Inserted some extra paragraphs in large proofs to make tex run...
|
changeset |
files
|
| Fri, 01 Nov 2002 10:35:50 +0100 |
kleing |
fixed "latex capacity exceeded"
|
changeset |
files
|
| 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.
|
changeset |
files
|
| Wed, 30 Oct 2002 12:44:18 +0100 |
paulson |
simpler separation/replacement proofs
|
changeset |
files
|
| Wed, 30 Oct 2002 12:18:23 +0100 |
nipkow |
modified msg
|
changeset |
files
|
| Tue, 29 Oct 2002 11:32:52 +0100 |
nipkow |
added induction thms
|
changeset |
files
|
| Mon, 28 Oct 2002 17:56:00 +0100 |
nipkow |
moved fac example
|
changeset |
files
|
| Mon, 28 Oct 2002 14:30:37 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Mon, 28 Oct 2002 14:29:51 +0100 |
nipkow |
conversion ML -> thy
|
changeset |
files
|
| Sun, 27 Oct 2002 23:34:02 +0100 |
kleing |
simplified lemma correct_frames_newref
|
changeset |
files
|
| Sat, 26 Oct 2002 13:05:27 +0200 |
isatest |
switched to atbroy51, removed markus from email list
|
changeset |
files
|