| Thu, 01 Oct 2009 16:09:47 +0200 |
wenzelm |
handle Pattern.MATCH, not arbitrary exceptions;
|
changeset |
files
|
| Thu, 01 Oct 2009 16:03:43 +0200 |
wenzelm |
more precise dependencies;
|
changeset |
files
|
| Thu, 01 Oct 2009 15:44:42 +0200 |
wenzelm |
eliminated redundant parameters;
|
changeset |
files
|
| Thu, 01 Oct 2009 14:27:50 +0200 |
wenzelm |
back to simple fold_body_thms and fulfill_proof/thm_proof (reverting a900d3cd47cc) -- the cycle check is implicit in the future computation of join_proofs;
|
changeset |
files
|
| Thu, 01 Oct 2009 14:11:28 +0200 |
wenzelm |
avoid mixed l/r infixes, which do not work in some versions of SML;
|
changeset |
files
|
| Thu, 01 Oct 2009 12:15:35 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 01 Oct 2009 11:33:32 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 01 Oct 2009 09:09:56 +0200 |
haftmann |
explicitly Unsynchronized
|
changeset |
files
|
| Thu, 01 Oct 2009 07:40:25 +0200 |
ballarin |
Merged.
|
changeset |
files
|
| Tue, 29 Sep 2009 22:15:54 +0200 |
ballarin |
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
|
changeset |
files
|
| Sun, 27 Sep 2009 11:50:27 +0200 |
ballarin |
Archive registrations by external view.
|
changeset |
files
|
| Sat, 26 Sep 2009 21:03:57 +0200 |
ballarin |
Stricter test: raise error if registration generates duplicate theorem.
|
changeset |
files
|
| Sat, 19 Sep 2009 18:43:11 +0200 |
ballarin |
Explicit management of registration mixins.
|
changeset |
files
|
| Wed, 19 Aug 2009 19:35:46 +0200 |
ballarin |
Improved comments and api names.
|
changeset |
files
|
| Thu, 01 Oct 2009 01:03:36 +0200 |
wenzelm |
eliminated dead code, redundant bindings and parameters;
|
changeset |
files
|
| Thu, 01 Oct 2009 00:32:00 +0200 |
wenzelm |
misc tuning and simplification;
|
changeset |
files
|
| Wed, 30 Sep 2009 23:49:53 +0200 |
wenzelm |
eliminated dead code;
|
changeset |
files
|
| Wed, 30 Sep 2009 23:44:23 +0200 |
wenzelm |
eliminated dead code;
|
changeset |
files
|
| Wed, 30 Sep 2009 23:30:37 +0200 |
wenzelm |
Sorts.of_sort_derivation: no pp here;
|
changeset |
files
|
| Wed, 30 Sep 2009 23:28:54 +0200 |
wenzelm |
eliminated redundant bindings;
|
changeset |
files
|
| Wed, 30 Sep 2009 23:16:15 +0200 |
wenzelm |
actually perform Isar_Document.init on startup;
|
changeset |
files
|
| Wed, 30 Sep 2009 23:13:18 +0200 |
wenzelm |
eliminated dead code;
|
changeset |
files
|
| Wed, 30 Sep 2009 22:53:33 +0200 |
wenzelm |
removed dead code;
|
changeset |
files
|
| Wed, 30 Sep 2009 22:31:16 +0200 |
wenzelm |
handle Type.TYPE_MATCH, not arbitrary exceptions;
|
changeset |
files
|
| Wed, 30 Sep 2009 22:27:20 +0200 |
wenzelm |
removed redundant Sign.certify_prop, use Sign.cert_prop instead;
|
changeset |
files
|
| Wed, 30 Sep 2009 22:26:47 +0200 |
wenzelm |
PARALLEL_GOALS: proper scope for exception FAILED, with dummy argument to prevent its interpretation as variable;
|
changeset |
files
|
| Wed, 30 Sep 2009 22:26:25 +0200 |
wenzelm |
actually export unit parser;
|
changeset |
files
|
| Wed, 30 Sep 2009 22:25:50 +0200 |
wenzelm |
eliminated dead code;
|
changeset |
files
|
| Wed, 30 Sep 2009 22:24:57 +0200 |
wenzelm |
eliminated redundant parameters;
|
changeset |
files
|
| Wed, 30 Sep 2009 22:20:58 +0200 |
wenzelm |
eliminated redundant bindings;
|
changeset |
files
|