| Mon, 03 Mar 2014 22:33:22 +0100 |
blanchet |
tuned ML names
|
changeset |
files
|
| Mon, 03 Mar 2014 22:33:22 +0100 |
blanchet |
tuned code
|
changeset |
files
|
| Mon, 03 Mar 2014 22:33:22 +0100 |
blanchet |
removed nonstandard models from Nitpick
|
changeset |
files
|
| Mon, 03 Mar 2014 16:44:46 +0100 |
nipkow |
more code lemmas by Rene Thiemann
|
changeset |
files
|
| Mon, 03 Mar 2014 15:14:00 +0100 |
wenzelm |
merged;
|
changeset |
files
|
| Mon, 03 Mar 2014 13:54:47 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Mon, 03 Mar 2014 12:54:12 +0100 |
wenzelm |
tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
|
changeset |
files
|
| Mon, 03 Mar 2014 12:24:14 +0100 |
wenzelm |
recovered position hyperlinks from 65c9968286d5 (NB: "def" position vs. regular one);
|
changeset |
files
|
| Mon, 03 Mar 2014 12:18:59 +0100 |
wenzelm |
tuned messages and markup;
|
changeset |
files
|
| Mon, 03 Mar 2014 12:14:47 +0100 |
wenzelm |
test polyml-svn;
|
changeset |
files
|
| Mon, 03 Mar 2014 11:58:55 +0100 |
wenzelm |
README is optional in test compilations;
|
changeset |
files
|
| Mon, 03 Mar 2014 11:58:07 +0100 |
wenzelm |
clarified path checks: avoid crash of rendering due to spurious errors;
|
changeset |
files
|
| Mon, 03 Mar 2014 11:37:06 +0100 |
wenzelm |
more precise navigation within open files;
|
changeset |
files
|
| Mon, 03 Mar 2014 10:59:33 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 03 Mar 2014 10:41:58 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 03 Mar 2014 14:22:35 +0100 |
blanchet |
updated NEWS
|
changeset |
files
|
| Mon, 03 Mar 2014 12:58:17 +0100 |
blanchet |
guard against unsound cases that arise when people peek into 'int' and similar types that are handled specially by Nitpick
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
adapted example
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
removed obsolete, harmful step in tactic
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
removed (co)iterators from documentation
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
avoid duplicate 'disc_iff' theorems
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
life without 'metis'
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalize internals
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
optimized simple non-recursive datatypes by reusing 'case' for 'rec' constant
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
compile
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
make 'diff_iff' a simp rule if available
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
less aggressive resolving
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
repaired argument list to corecursor
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
adapted to absence of 'unfold'
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
got rid of automatically generated fold constant and theorems (to reduce overhead)
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
use same identity function for abs and rep (doesn't seem to confuse any proofs)
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
make 'typedef' optional, depending on size of original type
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:19 +0100 |
blanchet |
use aconv to compare terms (for cleanliness)
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:19 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 03 Mar 2014 12:48:19 +0100 |
blanchet |
optimize cardinal bounds involving natLeq (omega)
|
changeset |
files
|
| Mon, 03 Mar 2014 03:13:45 +0100 |
wenzelm |
no extend_word for now, it is in conflict with manual reformatting of sources via TAB (e.g. accidental replacement of 'assume' by 'assumes');
|
changeset |
files
|
| Sun, 02 Mar 2014 22:43:20 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 02 Mar 2014 22:39:34 +0100 |
wenzelm |
more standard module name;
|
changeset |
files
|
| Sun, 02 Mar 2014 22:37:55 +0100 |
wenzelm |
silence warning due to addsimps @{thms dnf_simps}: duplicate not_not rule via simp_thms and nnf_simps;
|
changeset |
files
|
| Sun, 02 Mar 2014 22:24:52 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Sun, 02 Mar 2014 22:03:27 +0100 |
wenzelm |
allow suffix of underscores (usually unused names), to extend completion beyond already recognized entry;
|
changeset |
files
|
| Sun, 02 Mar 2014 21:52:44 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Sun, 02 Mar 2014 21:30:47 +0100 |
wenzelm |
prefer Name_Space.check with its builtin reports (including completion);
|
changeset |
files
|
| Sun, 02 Mar 2014 21:13:29 +0100 |
wenzelm |
tuned source structure;
|
changeset |
files
|
| Sun, 02 Mar 2014 21:02:27 +0100 |
wenzelm |
prefer Name_Space.check with its builtin reports (including completion);
|
changeset |
files
|
| Sun, 02 Mar 2014 20:34:11 +0100 |
wenzelm |
consider completion report as part of error message -- less stateful, may get handled;
|
changeset |
files
|
| Sun, 02 Mar 2014 20:20:20 +0100 |
wenzelm |
more markup for read_class: imitate Name_Space.check despite lack of Name_Space.table;
|
changeset |
files
|
| Sun, 02 Mar 2014 19:45:38 +0100 |
wenzelm |
more antiquotations;
|
changeset |
files
|
| Sun, 02 Mar 2014 19:00:45 +0100 |
wenzelm |
clarified names of antiquotations and markup;
|
changeset |
files
|
| Sun, 02 Mar 2014 19:15:23 +0100 |
nipkow |
tuned proof
|
changeset |
files
|
| Sun, 02 Mar 2014 18:41:41 +0100 |
nipkow |
merged
|
changeset |
files
|
| Sun, 02 Mar 2014 18:41:26 +0100 |
nipkow |
tuned proofs
|
changeset |
files
|
| Sun, 02 Mar 2014 18:20:08 +0100 |
wenzelm |
repaired document;
|
changeset |
files
|
| Sun, 02 Mar 2014 18:11:30 +0100 |
wenzelm |
repaired document;
|
changeset |
files
|
| Sun, 02 Mar 2014 00:05:35 +0100 |
wenzelm |
more markup for ML source;
|
changeset |
files
|