| Thu, 29 Apr 2010 07:02:22 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 28 Apr 2010 17:04:56 +0200 |
haftmann |
export somehow odd mapa explicitly
|
changeset |
files
|
| Wed, 28 Apr 2010 16:56:19 +0200 |
haftmann |
exported print_tuple
|
changeset |
files
|
| Wed, 28 Apr 2010 16:56:18 +0200 |
haftmann |
take into account tupled constructors
|
changeset |
files
|
| Wed, 28 Apr 2010 16:56:18 +0200 |
haftmann |
avoid code_datatype antiquotation
|
changeset |
files
|
| Wed, 28 Apr 2010 19:46:09 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Wed, 28 Apr 2010 16:45:51 +0200 |
bulwahn |
added an example with a free function variable to the Predicate Compile examples
|
changeset |
files
|
| Wed, 28 Apr 2010 16:45:50 +0200 |
bulwahn |
removed local clone in the predicate compiler
|
changeset |
files
|
| Wed, 28 Apr 2010 16:45:48 +0200 |
bulwahn |
improving proof procedure for transforming cases rule in the predicate compiler to handle free variables of function type
|
changeset |
files
|
| Thu, 29 Apr 2010 17:47:53 +0200 |
wenzelm |
allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
|
changeset |
files
|
| Thu, 29 Apr 2010 17:29:53 +0200 |
wenzelm |
'write': actually observe the proof structure (like 'let' or 'fix');
|
changeset |
files
|
| Thu, 29 Apr 2010 17:15:23 +0200 |
wenzelm |
adapted ProofContext.infer_type;
|
changeset |
files
|
| Thu, 29 Apr 2010 16:55:22 +0200 |
wenzelm |
ProofContext.read_const: allow for type constraint (for fixed variable);
|
changeset |
files
|
| Thu, 29 Apr 2010 16:53:08 +0200 |
wenzelm |
avoid clash with keyword 'write';
|
changeset |
files
|
| Thu, 29 Apr 2010 11:05:13 +0200 |
wenzelm |
allow mixfix syntax for fixes within a proof body -- should now work thanks to fully authentic syntax;
|
changeset |
files
|
| Thu, 29 Apr 2010 11:00:32 +0200 |
wenzelm |
uniform decoding of fixed/const syntax entities, allows to pass "\<^fixed>foo__" through the syntax layer (supersedes 1b7109c10b7b);
|
changeset |
files
|
| Wed, 28 Apr 2010 19:43:45 +0200 |
wenzelm |
disabled spurious invocation of (interactive) sledgehammer;
|
changeset |
files
|
| Wed, 28 Apr 2010 17:29:58 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 28 Apr 2010 16:56:03 +0200 |
blanchet |
make Mirabelle happy
|
changeset |
files
|
| Wed, 28 Apr 2010 16:47:56 +0200 |
blanchet |
remove removed option
|
changeset |
files
|
| Wed, 28 Apr 2010 16:15:45 +0200 |
blanchet |
merge
|
changeset |
files
|
| Wed, 28 Apr 2010 16:14:56 +0200 |
blanchet |
parentheses around nested cases
|
changeset |
files
|
| Wed, 28 Apr 2010 16:06:27 +0200 |
blanchet |
merged
|
changeset |
files
|
| Wed, 28 Apr 2010 16:05:38 +0200 |
blanchet |
add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)
|
changeset |
files
|