| Sun, 18 May 2014 17:01:31 +0200 |
wenzelm |
clarified dependencies -- Mavericks presently does not work;
|
changeset |
files
|
| Sun, 18 May 2014 00:00:26 +0200 |
wenzelm |
clarified docking layout, amending 9c2ca698690e;
|
changeset |
files
|
| Fri, 16 May 2014 19:14:00 +0200 |
blanchet |
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
|
changeset |
files
|
| Fri, 16 May 2014 19:13:50 +0200 |
blanchet |
removed needless transfer
|
changeset |
files
|
| Fri, 16 May 2014 19:13:50 +0200 |
blanchet |
use 'simp add:' syntax in Sledgehammer rather than 'using'
|
changeset |
files
|
| Fri, 16 May 2014 19:13:50 +0200 |
blanchet |
silence methods even better
|
changeset |
files
|
| Fri, 16 May 2014 19:13:50 +0200 |
blanchet |
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
|
changeset |
files
|
| Fri, 16 May 2014 17:11:56 +0200 |
wenzelm |
proper priority for error over warning, which got mixed up in 0546e036d1c0 and 4df2727a0b5f;
|
changeset |
files
|
| Fri, 16 May 2014 16:40:02 +0200 |
noschinl |
added lemmas for -1
|
changeset |
files
|
| Fri, 16 May 2014 12:56:39 +0200 |
blanchet |
proper handling of 'ctor_dtor' for mutual corecursive cases where not all type variables are present in all low-level constructors (cf. 'coind_wit1' etc. in 'Misc_Codatatypes.thy')
|
changeset |
files
|
| Fri, 16 May 2014 09:19:15 +0200 |
nipkow |
new syntax for card, normalized spacing for #
|
changeset |
files
|
| Thu, 15 May 2014 16:46:29 +0200 |
haftmann |
clarified stylized status of sandwich algebra
|
changeset |
files
|
| Thu, 15 May 2014 16:38:33 +0200 |
haftmann |
dropped dead code
|
changeset |
files
|
| Thu, 15 May 2014 16:38:32 +0200 |
haftmann |
accurate separation of static and dynamic context
|
changeset |
files
|
| Thu, 15 May 2014 16:38:31 +0200 |
haftmann |
syntactic means to prevent accidental mixup of static and dynamic context
|
changeset |
files
|
| Thu, 15 May 2014 16:38:31 +0200 |
haftmann |
proper separation of static and dynamic context
|
changeset |
files
|
| Thu, 15 May 2014 16:38:30 +0200 |
haftmann |
optimization for trivial cases
|
changeset |
files
|
| Thu, 15 May 2014 16:38:29 +0200 |
haftmann |
modernized setup
|
changeset |
files
|
| Thu, 15 May 2014 16:38:29 +0200 |
haftmann |
dropped obsolete hand-waving adjustion of type variables: safely done in preprocessor
|
changeset |
files
|
| Thu, 15 May 2014 16:38:28 +0200 |
haftmann |
unified approach toward conversions and simple term rewriting in preprocessor by means of sandwiches
|
changeset |
files
|
| Thu, 15 May 2014 16:38:17 +0200 |
haftmann |
normalize type variables of evaluation term by conversion
|
changeset |
files
|
| Thu, 15 May 2014 20:48:14 +0200 |
blanchet |
more aggressive nested size handling in the absence of 'size_o_map' theorems (+ unrelated pattern matching fix)
|
changeset |
files
|
| Thu, 15 May 2014 20:48:13 +0200 |
blanchet |
new approach to silence proof methods, to avoid weird theory/context mismatches
|
changeset |
files
|
| Thu, 15 May 2014 18:18:50 +0200 |
haftmann |
type
|
changeset |
files
|
| Wed, 14 May 2014 13:36:35 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 14 May 2014 13:10:57 +0200 |
wenzelm |
restrict default docking layout to bare minimum -- NB: Simplifier Trace still needs fine-tuning to show up on demand;
|
changeset |
files
|
| Wed, 14 May 2014 13:07:47 +0200 |
wenzelm |
updated isatest;
|
changeset |
files
|
| Wed, 14 May 2014 12:24:38 +0200 |
wenzelm |
updated to polyml-5.5.2;
|
changeset |
files
|