| Sun, 15 Dec 2013 22:03:12 +0100 |
blanchet |
generate proper succedent for cases with trivial branches
|
changeset |
files
|
| Sun, 15 Dec 2013 20:31:25 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Sun, 15 Dec 2013 20:09:13 +0100 |
blanchet |
simplify generated propositions
|
changeset |
files
|
| Sun, 15 Dec 2013 19:01:06 +0100 |
blanchet |
use 'prop' rather than 'bool' systematically in Isar reconstruction code
|
changeset |
files
|
| Sun, 15 Dec 2013 18:54:26 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Sun, 15 Dec 2013 18:01:38 +0100 |
blanchet |
use 'arith' when appropriate in Z3 proofs
|
changeset |
files
|
| Sun, 15 Dec 2013 18:01:38 +0100 |
blanchet |
robustness in degenerate case + tuning
|
changeset |
files
|
| Sun, 15 Dec 2013 18:01:38 +0100 |
blanchet |
use simplifier for rewrite
|
changeset |
files
|
| Sun, 15 Dec 2013 18:01:38 +0100 |
blanchet |
more aggressive merging
|
changeset |
files
|
| Sun, 15 Dec 2013 18:01:38 +0100 |
blanchet |
implemented Z3 skolemization
|
changeset |
files
|
| Sun, 15 Dec 2013 18:01:38 +0100 |
blanchet |
inline Z3 hypotheses
|
changeset |
files
|
| Sun, 15 Dec 2013 18:01:35 +0100 |
blanchet |
merge
|
changeset |
files
|
| Sun, 15 Dec 2013 05:11:46 +0100 |
blanchet |
merge
|
changeset |
files
|
| Sat, 14 Dec 2013 07:45:30 +0800 |
blanchet |
merged
|
changeset |
files
|
| Sat, 14 Dec 2013 07:26:45 +0800 |
blanchet |
better handling of Z3 proof blocks
|
changeset |
files
|
| Sun, 15 Dec 2013 15:10:16 +0100 |
haftmann |
disambiguation of interpretation prefixes
|
changeset |
files
|
| Sun, 15 Dec 2013 15:10:14 +0100 |
haftmann |
more algebraic terminology for theories about big operators
|
changeset |
files
|
| Sat, 14 Dec 2013 20:46:36 +0100 |
wenzelm |
more antiquotations;
|
changeset |
files
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
changeset |
files
|
| Fri, 13 Dec 2013 23:53:02 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 13 Dec 2013 20:20:15 +0100 |
wenzelm |
maintain morphism names for diagnostic purposes;
|
changeset |
files
|
| Fri, 13 Dec 2013 14:58:47 +0100 |
wenzelm |
tuned -- prefer canonical argument order of fold_rev;
|
changeset |
files
|
| Fri, 13 Dec 2013 14:15:52 +0100 |
wenzelm |
proper simplifier context;
|
changeset |
files
|
| Fri, 13 Dec 2013 14:09:51 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 13 Dec 2013 13:59:01 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Fri, 13 Dec 2013 22:54:39 +0800 |
blanchet |
made SML/NJ happy + whitespace tuning
|
changeset |
files
|
| Fri, 13 Dec 2013 12:31:45 +0100 |
wenzelm |
clarified Proof General legacy: special treatment of \<^newline> only in TTY mode;
|
changeset |
files
|
| Thu, 12 Dec 2013 23:18:47 +0100 |
wenzelm |
merged
|
changeset |
files
|