| Sat, 29 Jul 2006 13:15:12 +0200 |
webertj |
lin_arith_prover splits certain operators (e.g. min, max, abs)
|
changeset |
files
|
| Sat, 29 Jul 2006 00:51:36 +0200 |
wenzelm |
rename legacy_pretty_thm to pretty_thm_legacy;
|
changeset |
files
|
| Sat, 29 Jul 2006 00:51:34 +0200 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Sat, 29 Jul 2006 00:51:33 +0200 |
wenzelm |
added add_fixes_direct;
|
changeset |
files
|
| Sat, 29 Jul 2006 00:51:32 +0200 |
wenzelm |
prove: proper assumption context, more tactic arguments;
|
changeset |
files
|
| Sat, 29 Jul 2006 00:51:31 +0200 |
wenzelm |
added mk_conjunction_list;
|
changeset |
files
|
| Sat, 29 Jul 2006 00:51:29 +0200 |
wenzelm |
Goal.prove: more tactic arguments;
|
changeset |
files
|
| Fri, 28 Jul 2006 18:37:25 +0200 |
paulson |
Checking for unsound proofs. Tidying.
|
changeset |
files
|
| Fri, 28 Jul 2006 18:36:24 +0200 |
paulson |
"all theorems" mode forces definition-expansion off.
|
changeset |
files
|
| Fri, 28 Jul 2006 18:11:22 +0200 |
webertj |
title fixed
|
changeset |
files
|
| Thu, 27 Jul 2006 23:28:30 +0200 |
wenzelm |
replaced extern_skolem by slightly more simplistic revert_skolems;
|
changeset |
files
|
| Thu, 27 Jul 2006 23:28:28 +0200 |
wenzelm |
renamed ProofContext.fix_frees to Variable.fix_frees;
|
changeset |
files
|
| Thu, 27 Jul 2006 23:28:27 +0200 |
wenzelm |
replaced ProofContext.extern_skolem by slightly more simplistic ProofContext.revert_skolems;
|
changeset |
files
|
| Thu, 27 Jul 2006 23:28:26 +0200 |
wenzelm |
no_vars: based on Variable.import;
|
changeset |
files
|
| Thu, 27 Jul 2006 23:28:25 +0200 |
wenzelm |
added fix_frees (from Isar/proof_context.ML);
|
changeset |
files
|