| Fri, 13 Dec 2002 18:14:25 +0100 |
oheimb |
cent/currency: changed from wasysym to textcomp because of PDF problems
|
changeset |
files
|
| Fri, 13 Dec 2002 16:49:08 +0100 |
paulson |
trace_unify_fail
|
changeset |
files
|
| Fri, 13 Dec 2002 16:48:20 +0100 |
paulson |
integer induction rules
|
changeset |
files
|
| Fri, 13 Dec 2002 14:20:47 +0100 |
berghofe |
size_of_proof no longer includes size_of_term
|
changeset |
files
|
| Fri, 13 Dec 2002 13:47:13 +0100 |
paulson |
deleted redundant line
|
changeset |
files
|
| Thu, 12 Dec 2002 11:38:18 +0100 |
paulson |
Better treatment of equality in premises of inductive definitions. Less
|
changeset |
files
|
| Thu, 12 Dec 2002 11:33:48 +0100 |
ballarin |
Fixed error that affected document preperation.
|
changeset |
files
|
| Wed, 11 Dec 2002 10:12:48 +0100 |
ballarin |
HOL/GroupTheory/Summation.thy added: summation operator for abelian groups.
|
changeset |
files
|
| Tue, 10 Dec 2002 10:40:32 +0100 |
berghofe |
Added size_of_proof.
|
changeset |
files
|
| Mon, 09 Dec 2002 10:38:56 +0100 |
ballarin |
Fixed bug in simpdata.ML that prevented the use of congruence rules from a
|
changeset |
files
|
| Fri, 06 Dec 2002 15:16:30 +0100 |
oheimb |
corrected swallowing of newlines after end-of-ignore
|
changeset |
files
|
| Fri, 06 Dec 2002 11:09:02 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Thu, 05 Dec 2002 18:44:16 +0100 |
kleing |
for dvi target
|
changeset |
files
|
| 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
|
| Fri, 25 Oct 2002 10:47:47 +0200 |
kleing |
fixed latex output
|
changeset |
files
|
| Thu, 24 Oct 2002 12:08:33 +0200 |
kleing |
changes for cleanup in JVM
|
changeset |
files
|
| Thu, 24 Oct 2002 12:07:31 +0200 |
kleing |
cleanup, beautified
|
changeset |
files
|
| Thu, 24 Oct 2002 12:06:43 +0200 |
kleing |
fixed latex error
|
changeset |
files
|
| Thu, 24 Oct 2002 07:23:46 +0200 |
nipkow |
ASIN -> SET
|
changeset |
files
|
| Wed, 23 Oct 2002 16:10:42 +0200 |
streckem |
*** empty log message ***
|
changeset |
files
|
| Wed, 23 Oct 2002 16:10:02 +0200 |
streckem |
First checkin of compiler
|
changeset |
files
|
| Wed, 23 Oct 2002 16:09:02 +0200 |
streckem |
Added compiler
|
changeset |
files
|
| Mon, 21 Oct 2002 17:23:23 +0200 |
berghofe |
Eta contraction is now switched off when printing extracted program.
|
changeset |
files
|
| Mon, 21 Oct 2002 17:20:29 +0200 |
berghofe |
Fixed problem with theorems containing TFrees.
|
changeset |
files
|
| Mon, 21 Oct 2002 17:19:51 +0200 |
berghofe |
- reconstruct_proof no longer relies on TypeInfer.infer_types
|
changeset |
files
|
| Mon, 21 Oct 2002 17:17:40 +0200 |
berghofe |
Removed Logic.skip_flexpairs.
|
changeset |
files
|
| Mon, 21 Oct 2002 17:16:24 +0200 |
berghofe |
Replaced variantlist (quadratic) by gen_names (linear).
|
changeset |
files
|
| Mon, 21 Oct 2002 17:15:40 +0200 |
berghofe |
Removed add_env because Vartab.map was too slow for large environments.
|
changeset |
files
|
| Mon, 21 Oct 2002 17:14:19 +0200 |
berghofe |
- removed flexpair
|
changeset |
files
|
| Mon, 21 Oct 2002 17:12:44 +0200 |
berghofe |
No more explicit manipulation of flex-flex constraints in metahyps_aux_tac.
|
changeset |
files
|
| Mon, 21 Oct 2002 17:11:29 +0200 |
berghofe |
Removed flexpair_def.
|
changeset |
files
|
| Mon, 21 Oct 2002 17:11:06 +0200 |
berghofe |
Removed Logic.strip_flexpairs.
|
changeset |
files
|
| Mon, 21 Oct 2002 17:09:31 +0200 |
berghofe |
No more explicit manipulation of flex-flex constraints in goals_conv.
|
changeset |
files
|
| Mon, 21 Oct 2002 17:07:58 +0200 |
berghofe |
Changed type of Logic.strip_horn.
|
changeset |
files
|
| Mon, 21 Oct 2002 17:07:27 +0200 |
berghofe |
Removed obsolete functions dealing with flex-flex constraints.
|
changeset |
files
|
| Mon, 21 Oct 2002 17:04:47 +0200 |
berghofe |
Changed handling of flex-flex constraints: now stored in separate
|
changeset |
files
|
| Mon, 21 Oct 2002 17:00:45 +0200 |
berghofe |
Now applies standard' to "unfold" theorem (due to flex-flex constraints).
|
changeset |
files
|