| 2013-08-09 |
wenzelm |
sorted lines;
|
changeset |
files
|
| 2013-08-09 |
wenzelm |
tuned GUI;
|
changeset |
files
|
| 2013-08-09 |
wenzelm |
retain current task priority, to avoid distortion due to local forks (e.g. sledgehammer query operation);
|
changeset |
files
|
| 2013-08-09 |
wenzelm |
removed "Locate" button, to avoid confusion about the slightly odd meaning of current_command with explicit theory context;
|
changeset |
files
|
| 2013-08-09 |
wenzelm |
enable search in pre-loaded theory;
|
changeset |
files
|
| 2013-08-09 |
wenzelm |
more GUI options;
|
changeset |
files
|
| 2013-08-09 |
wenzelm |
tuned signature;
|
changeset |
files
|
| 2013-08-09 |
wenzelm |
tuned;
|
changeset |
files
|
| 2013-08-09 |
wenzelm |
tuned GUI;
|
changeset |
files
|
| 2013-08-09 |
blanchet |
tuned name generation code (to make it easier to adapt later)
|
changeset |
files
|
| 2013-08-09 |
blanchet |
honor user type names if possible
|
changeset |
files
|
| 2013-08-09 |
wenzelm |
merged;
|
changeset |
files
|
| 2013-08-09 |
wenzelm |
more abstract consume_status operation;
|
changeset |
files
|
| 2013-08-09 |
wenzelm |
separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;
|
changeset |
files
|
| 2013-08-09 |
wenzelm |
more active "provers" field, which increases chances that its history is stored;
|
changeset |
files
|
| 2013-08-09 |
wenzelm |
removed command location is considered finished, and its overlay removed eventually;
|
changeset |
files
|
| 2013-08-09 |
wenzelm |
cancel_query via direct access to the exec_id of the running query process;
|
changeset |
files
|
| 2013-08-09 |
wenzelm |
retain original messages properties, e.g. for retrieval via Command.Results;
|
changeset |
files
|
| 2013-08-09 |
wenzelm |
clarified toplevel_error: absorb and print interrupts;
|
changeset |
files
|
| 2013-08-08 |
wenzelm |
more explicit error;
|
changeset |
files
|
| 2013-08-08 |
wenzelm |
tuned message;
|
changeset |
files
|
| 2013-08-08 |
wenzelm |
removed unused YXML_Find_Theorems and Legacy_XML_Syntax;
|
changeset |
files
|
| 2013-08-08 |
wenzelm |
more robust read_query;
|
changeset |
files
|
| 2013-08-09 |
kleing |
removed commented out declaration
|
changeset |
files
|
| 2013-08-09 |
traytel |
tuned
|
changeset |
files
|
| 2013-08-08 |
wenzelm |
merged
|
changeset |
files
|
| 2013-08-08 |
wenzelm |
eliminate \<twosuperior> as well;
|
changeset |
files
|
| 2013-08-08 |
wenzelm |
more strict identifier syntax: disallow superscripts, which tend to be used in notation such as \<^sup>\<omega>;
|
changeset |
files
|
| 2013-08-08 |
wenzelm |
prefer plain subscript for identifiers;
|
changeset |
files
|
| 2013-08-08 |
wenzelm |
proper low-level comparison -- heed warning by Scala compiler;
|
changeset |
files
|
| 2013-08-08 |
Andreas Lochbihler |
merged
|
changeset |
files
|
| 2013-08-08 |
Andreas Lochbihler |
prefer Code.abort with explicit error message
|
changeset |
files
|
| 2013-08-08 |
kleing |
avoid re-inventing transitive closure
|
changeset |
files
|
| 2013-08-08 |
traytel |
merged
|
changeset |
files
|
| 2013-08-08 |
traytel |
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
|
changeset |
files
|
| 2013-08-08 |
traytel |
tuned
|
changeset |
files
|
| 2013-08-08 |
traytel |
tuned tactic;
|
changeset |
files
|
| 2013-08-08 |
Andreas Lochbihler |
abort execution of generated code with explicit exception message
|
changeset |
files
|
| 2013-08-08 |
wenzelm |
merged
|
changeset |
files
|
| 2013-08-08 |
wenzelm |
dockable window for Sledgehammer, based on asynchronous/parallel query operation;
|
changeset |
files
|
| 2013-08-08 |
wenzelm |
tuned imports;
|
changeset |
files
|
| 2013-08-08 |
kleing |
snippet for instr type
|
changeset |
files
|
| 2013-08-08 |
traytel |
filter function on streams
|
changeset |
files
|
| 2013-08-08 |
traytel |
tuned
|
changeset |
files
|
| 2013-08-07 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| 2013-08-07 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| 2013-08-07 |
wenzelm |
maintain commands together with index -- avoid redundant reconstruction of full_index;
|
changeset |
files
|
| 2013-08-07 |
wenzelm |
more elementary list structures for markup tree traversal;
|
changeset |
files
|
| 2013-08-07 |
blanchet |
tuning
|
changeset |
files
|
| 2013-08-07 |
blanchet |
enrich exported ML function's signature
|
changeset |
files
|
| 2013-08-07 |
wenzelm |
merged
|
changeset |
files
|
| 2013-08-07 |
wenzelm |
more NEWS and CONTRIBUTORS;
|
changeset |
files
|
| 2013-08-02 |
Christian Sternagel |
some documentation for adhoc overloading;
|
changeset |
files
|
| 2013-08-02 |
Christian Sternagel |
added examples of adhoc overloading
|
changeset |
files
|
| 2013-08-02 |
Christian Sternagel |
use uniform spelling of "adhoc"
|
changeset |
files
|
| 2013-08-02 |
Christian Sternagel |
tuned formatting of error message
|
changeset |
files
|
| 2013-08-07 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| 2013-08-07 |
wenzelm |
tuned signature;
|
changeset |
files
|
| 2013-08-07 |
wenzelm |
more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
|
changeset |
files
|
| 2013-08-07 |
wenzelm |
tuned;
|
changeset |
files
|