| 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
|
| Mon, 21 Oct 2002 16:57:39 +0200 |
berghofe |
Changed type of Logic.strip_horn.
|
changeset |
files
|
| Fri, 18 Oct 2002 17:50:13 +0200 |
paulson |
Tidying up. New primitives is_iterates and is_iterates_fm.
|
changeset |
files
|
| Fri, 18 Oct 2002 09:53:18 +0200 |
nipkow |
Mod due to: Added a few thms about UN/INT/{}/UNIV
|
changeset |
files
|
| Fri, 18 Oct 2002 09:53:02 +0200 |
nipkow |
Added a few thms about UN/INT/{}/UNIV
|
changeset |
files
|
| Thu, 17 Oct 2002 10:56:00 +0200 |
paulson |
fixed comments and types
|
changeset |
files
|
| Thu, 17 Oct 2002 10:54:11 +0200 |
paulson |
Cosmetic changes suggested by writing the paper. Deleted some
|
changeset |
files
|
| Thu, 17 Oct 2002 10:52:59 +0200 |
paulson |
fixing the cut_tac method to work when there are no instantiations and the
|
changeset |
files
|
| Tue, 15 Oct 2002 15:37:57 +0200 |
kleing |
alternative syntax
|
changeset |
files
|
| Mon, 14 Oct 2002 13:35:17 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Mon, 14 Oct 2002 11:32:00 +0200 |
paulson |
tidying and reorganization
|
changeset |
files
|
| Mon, 14 Oct 2002 10:44:32 +0200 |
nipkow |
Ported find_intro/elim to Isar.
|
changeset |
files
|
| Fri, 11 Oct 2002 12:47:52 +0200 |
berghofe |
norm_typ -> Envir.norm_type
|
changeset |
files
|
| Thu, 10 Oct 2002 19:24:34 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Thu, 10 Oct 2002 19:03:37 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Thu, 10 Oct 2002 19:02:23 +0200 |
nipkow |
added failure trace information to pattern unification
|
changeset |
files
|
| Thu, 10 Oct 2002 14:26:50 +0200 |
berghofe |
Reimplemented parts of datatype package dealing with datatypes involving
|
changeset |
files
|
| Thu, 10 Oct 2002 14:23:47 +0200 |
berghofe |
Added list_all.
|
changeset |
files
|
| Thu, 10 Oct 2002 14:23:19 +0200 |
berghofe |
Removed obsolete function "fun_rel_comp".
|
changeset |
files
|
| Thu, 10 Oct 2002 14:21:49 +0200 |
berghofe |
Added choice_eq.
|
changeset |
files
|
| Thu, 10 Oct 2002 14:21:20 +0200 |
berghofe |
- Added range_ex1_eq
|
changeset |
files
|
| Thu, 10 Oct 2002 14:19:17 +0200 |
berghofe |
Removed obsolete function "Funs".
|
changeset |
files
|
| Thu, 10 Oct 2002 14:18:01 +0200 |
berghofe |
Added functions Suml and Sumr which are useful for constructing
|
changeset |
files
|
| Wed, 09 Oct 2002 11:07:13 +0200 |
paulson |
Re-organization of Constructible theories
|
changeset |
files
|
| Tue, 08 Oct 2002 14:09:18 +0200 |
kleing |
type safety with defensive machine
|
changeset |
files
|
| Tue, 08 Oct 2002 14:08:50 +0200 |
kleing |
defensive machine
|
changeset |
files
|
| Tue, 08 Oct 2002 10:49:19 +0200 |
kleing |
defensive machine without obj init and jsr
|
changeset |
files
|
| Tue, 08 Oct 2002 08:20:17 +0200 |
nipkow |
Got rid of rotates because of new simplifier
|
changeset |
files
|
| Mon, 07 Oct 2002 19:01:51 +0200 |
nipkow |
take/drop -> splitAt
|
changeset |
files
|
| Fri, 04 Oct 2002 15:57:32 +0200 |
paulson |
Various simplifications of the Constructible theories
|
changeset |
files
|
| Fri, 04 Oct 2002 15:23:58 +0200 |
paulson |
Fixed bug involving inductive definitions with equalities in the premises.
|
changeset |
files
|
| Fri, 04 Oct 2002 15:23:12 +0200 |
paulson |
Fixed bug involving inductive definitions having equalities in the premises,
|
changeset |
files
|
| Fri, 04 Oct 2002 09:56:48 +0200 |
berghofe |
Documented new "asm_lr" option for simp.
|
changeset |
files
|
| Thu, 03 Oct 2002 10:34:51 +0200 |
paulson |
added the new elim rule psubsetE
|
changeset |
files
|
| Thu, 03 Oct 2002 09:54:54 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 02 Oct 2002 17:25:31 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 02 Oct 2002 17:03:51 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 02 Oct 2002 15:26:07 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Tue, 01 Oct 2002 20:54:17 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Tue, 01 Oct 2002 15:03:28 +0200 |
berghofe |
Added some comments on new simplifier.
|
changeset |
files
|
| Tue, 01 Oct 2002 14:45:28 +0200 |
berghofe |
Documented new "asm_lr" option for simp.
|
changeset |
files
|
| Tue, 01 Oct 2002 14:44:43 +0200 |
berghofe |
Adapted to new simplifier.
|
changeset |
files
|
| Tue, 01 Oct 2002 13:26:10 +0200 |
paulson |
Numerous cosmetic changes, prompted by the new simplifier
|
changeset |
files
|
| Tue, 01 Oct 2002 11:17:25 +0200 |
berghofe |
Deleted superfluous dest_implies.
|
changeset |
files
|
| Mon, 30 Sep 2002 16:50:39 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Mon, 30 Sep 2002 16:48:15 +0200 |
berghofe |
Adapted to new simplifier.
|
changeset |
files
|
| Mon, 30 Sep 2002 16:47:03 +0200 |
berghofe |
Adapted to new simplifier.
|
changeset |
files
|
| Mon, 30 Sep 2002 16:44:00 +0200 |
berghofe |
Fixed bug in expand_proof which caused indexes to be incremented incorrectly.
|
changeset |
files
|
| Mon, 30 Sep 2002 16:42:46 +0200 |
berghofe |
Added check for axioms with "realizes Null A = A".
|
changeset |
files
|
| Mon, 30 Sep 2002 16:40:57 +0200 |
berghofe |
Added function elim_vars.
|
changeset |
files
|
| Mon, 30 Sep 2002 16:38:22 +0200 |
berghofe |
Completely reimplemented mutual simplification of premises.
|
changeset |
files
|
| Mon, 30 Sep 2002 16:37:44 +0200 |
berghofe |
Removed nRS again because extract_rews now takes care of preserving names.
|
changeset |
files
|
| Mon, 30 Sep 2002 16:36:57 +0200 |
berghofe |
Added syntax for "asm_lr" simplifier option.
|
changeset |
files
|
| Mon, 30 Sep 2002 16:34:56 +0200 |
berghofe |
- eliminated thin_leading_eqs_tac
|
changeset |
files
|
| Mon, 30 Sep 2002 16:32:05 +0200 |
berghofe |
Introduced addss', which adds asm_lr_simp_tac as a wrapper to the claset.
|
changeset |
files
|
| Mon, 30 Sep 2002 16:27:38 +0200 |
berghofe |
- additional congruence rules for boolean operators
|
changeset |
files
|
| Mon, 30 Sep 2002 16:14:02 +0200 |
berghofe |
Adapted to new simplifier.
|
changeset |
files
|
| Mon, 30 Sep 2002 16:12:16 +0200 |
berghofe |
Removed nRS again because extract_rews now takes care of preserving names.
|
changeset |
files
|
| Mon, 30 Sep 2002 16:10:32 +0200 |
berghofe |
Added elim_vars to preprocessor.
|
changeset |
files
|
| Mon, 30 Sep 2002 16:09:05 +0200 |
berghofe |
Fixed problem with induct_conj_curry: variable C should have type prop.
|
changeset |
files
|
| Mon, 30 Sep 2002 15:45:11 +0200 |
nipkow |
fixes !!-bound vars in induction statement automatically
|
changeset |
files
|
| Mon, 30 Sep 2002 15:44:21 +0200 |
nipkow |
modified induct method
|
changeset |
files
|
| Fri, 27 Sep 2002 16:44:50 +0200 |
paulson |
Proof tidying
|
changeset |
files
|
| Fri, 27 Sep 2002 13:24:29 +0200 |
paulson |
Isar experiments, etc.
|
changeset |
files
|
| Fri, 27 Sep 2002 10:36:21 +0200 |
paulson |
Tidied. New Pi-theorem.
|
changeset |
files
|
| Fri, 27 Sep 2002 10:35:10 +0200 |
paulson |
new Ring example
|
changeset |
files
|
| Fri, 27 Sep 2002 10:35:01 +0200 |
paulson |
Isar proof
|
changeset |
files
|
| Fri, 27 Sep 2002 10:34:05 +0200 |
paulson |
Modules theory added
|
changeset |
files
|
| Fri, 27 Sep 2002 10:33:47 +0200 |
paulson |
New theory GroupTheory/Module.thy of modules
|
changeset |
files
|
| Thu, 26 Sep 2002 15:21:38 +0200 |
paulson |
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
|
changeset |
files
|
| Thu, 26 Sep 2002 10:56:20 +0200 |
paulson |
GroupTheory and FuncSet
|
changeset |
files
|
| Thu, 26 Sep 2002 10:51:58 +0200 |
paulson |
new theory for Pi-sets, restrict, etc.
|
changeset |
files
|
| Thu, 26 Sep 2002 10:51:29 +0200 |
paulson |
Converted Fun to Isar style.
|
changeset |
files
|
| Thu, 26 Sep 2002 10:43:43 +0200 |
paulson |
new document directory for GroupTheory
|
changeset |
files
|
| Thu, 26 Sep 2002 10:40:13 +0200 |
paulson |
converted to Isar and using new "implicit structures" instead of Sigma, etc
|
changeset |
files
|