| Wed, 19 Jul 2006 12:12:08 +0200 |
wenzelm |
export is_tid;
|
changeset |
files
|
| Wed, 19 Jul 2006 12:12:07 +0200 |
wenzelm |
thm_of_proof: improved generation of variables;
|
changeset |
files
|
| Wed, 19 Jul 2006 12:12:06 +0200 |
wenzelm |
Sign.infer_types: Name.context;
|
changeset |
files
|
| Wed, 19 Jul 2006 12:12:05 +0200 |
wenzelm |
reorganize declarations (more efficient);
|
changeset |
files
|
| Wed, 19 Jul 2006 12:12:04 +0200 |
wenzelm |
Name.context for used'';
|
changeset |
files
|
| Wed, 19 Jul 2006 12:12:03 +0200 |
wenzelm |
added variant_frees;
|
changeset |
files
|
| Wed, 19 Jul 2006 12:12:02 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 19 Jul 2006 12:12:01 +0200 |
wenzelm |
export make_context, is_declared;
|
changeset |
files
|
| Wed, 19 Jul 2006 12:12:00 +0200 |
wenzelm |
prove: Variable.declare_internal (more efficient);
|
changeset |
files
|
| Wed, 19 Jul 2006 12:11:59 +0200 |
wenzelm |
add_local: simplified interface, all frees are known'';
|
changeset |
files
|
| Wed, 19 Jul 2006 12:11:57 +0200 |
wenzelm |
Sign.infer_types: Name.context;
|
changeset |
files
|
| Wed, 19 Jul 2006 12:11:56 +0200 |
wenzelm |
renamed Variable.rename_wrt to Variable.variant_frees;
|
changeset |
files
|
| Wed, 19 Jul 2006 11:55:26 +0200 |
paulson |
Fixed the bugs introduced by the last commit! Output is now *identical* to that
|
changeset |
files
|
| Wed, 19 Jul 2006 02:35:22 +0200 |
webertj |
MiniSat proof trace format changed; MiniSat is now expected to produce a proof also for "trivial" problems
|
changeset |
files
|