| Wed, 25 Mar 2009 21:34:31 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 25 Mar 2009 17:23:44 +0100 |
wenzelm |
use more informative Thm.proof_body_of for oracle demo;
|
changeset |
files
|
| Wed, 25 Mar 2009 16:54:49 +0100 |
wenzelm |
Proofterm.approximate_proof_body;
|
changeset |
files
|
| Wed, 25 Mar 2009 16:54:17 +0100 |
wenzelm |
fulfill_proof/thm_proof: pass whole proof_body, not just the projection to proof (which might be incomplete);
|
changeset |
files
|
| Wed, 25 Mar 2009 16:52:50 +0100 |
wenzelm |
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
|
changeset |
files
|
| Wed, 25 Mar 2009 14:47:08 +0100 |
wenzelm |
avoid mixing of left/right associative infixes, to make it work with experimental Poly/ML 5.3 branch;
|
changeset |
files
|
| Tue, 24 Mar 2009 23:43:58 +0100 |
wenzelm |
simplified addPrettyPrinter setup: may pass (fn ...) directly if type constraints are omitted -- addPrettyPrinter treated as a special case internally;
|
changeset |
files
|
| Tue, 24 Mar 2009 22:56:17 +0100 |
wenzelm |
status_of: need to include local promises as well!
|
changeset |
files
|
| Tue, 24 Mar 2009 22:55:49 +0100 |
wenzelm |
status_of: simultaneous list;
|
changeset |
files
|
| Tue, 24 Mar 2009 21:24:53 +0100 |
wenzelm |
display derivation status of thms;
|
changeset |
files
|
| Tue, 24 Mar 2009 19:37:50 +0100 |
wenzelm |
recover old ids;
|
changeset |
files
|
| Tue, 24 Mar 2009 18:21:58 +0100 |
wenzelm |
report ML typing;
|
changeset |
files
|
| Tue, 24 Mar 2009 16:11:42 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 24 Mar 2009 14:09:24 +0100 |
nipkow |
merged
|
changeset |
files
|
| Tue, 24 Mar 2009 14:08:13 +0100 |
nipkow |
NEWS: [arith]
|
changeset |
files
|
| Tue, 24 Mar 2009 16:11:09 +0100 |
wenzelm |
get_index: produce index of next pending token, not the last one;
|
changeset |
files
|
| Tue, 24 Mar 2009 15:47:55 +0100 |
wenzelm |
register token positions persistently with context;
|
changeset |
files
|
| Tue, 24 Mar 2009 15:43:37 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 24 Mar 2009 15:43:13 +0100 |
wenzelm |
more markup elements for ML programs;
|
changeset |
files
|
| Tue, 24 Mar 2009 13:20:40 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 24 Mar 2009 13:12:23 +0100 |
wenzelm |
process at-sml-dev last -- takes very long (why?);
|
changeset |
files
|
| Tue, 24 Mar 2009 13:13:18 +0100 |
nipkow |
fix
|
changeset |
files
|
| Tue, 24 Mar 2009 12:45:23 +0100 |
nipkow |
merged
|
changeset |
files
|
| Tue, 24 Mar 2009 12:45:01 +0100 |
nipkow |
presburger uses [arith] now
|
changeset |
files
|
| Tue, 24 Mar 2009 12:01:12 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 24 Mar 2009 09:15:59 +0100 |
haftmann |
merged
|
changeset |
files
|
| Tue, 24 Mar 2009 09:15:51 +0100 |
haftmann |
added Imperative_HOL_ex
|
changeset |
files
|
| Tue, 24 Mar 2009 15:55:11 +1100 |
Timothy Bourke |
Use assms rather than prems in find_theorems solves.
|
changeset |
files
|