| Fri, 19 Dec 2014 11:18:00 +0100 |
desharna |
document 'case_distrib'
|
changeset |
files
|
| Mon, 05 Jan 2015 06:56:15 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 19 Dec 2014 11:17:23 +0100 |
desharna |
generate 'case_distrib' for Ctr_Sugars
|
changeset |
files
|
| Mon, 05 Jan 2015 00:07:01 +0100 |
wenzelm |
more metrics, with integer coordinates for layout;
|
changeset |
files
|
| Sun, 04 Jan 2015 21:53:05 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 04 Jan 2015 21:29:52 +0100 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Sun, 04 Jan 2015 21:01:27 +0100 |
wenzelm |
explicit Layout.Point;
|
changeset |
files
|
| Sun, 04 Jan 2015 16:45:41 +0100 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Sun, 04 Jan 2015 15:23:23 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 04 Jan 2015 14:05:24 +0100 |
wenzelm |
clarified static full_graph vs. dynamic visible_graph;
|
changeset |
files
|
| Sun, 04 Jan 2015 13:34:42 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 03 Jan 2015 22:56:46 +0100 |
wenzelm |
tuned -- more iterators;
|
changeset |
files
|
| Sat, 03 Jan 2015 22:34:18 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 03 Jan 2015 22:04:31 +0100 |
wenzelm |
clarified fit_to_window: floor scale within window bounds;
|
changeset |
files
|
| Sat, 03 Jan 2015 21:50:50 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 03 Jan 2015 21:24:16 +0100 |
wenzelm |
apply_layout: proper repaint;
|
changeset |
files
|
| Sat, 03 Jan 2015 21:12:54 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 03 Jan 2015 21:07:05 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 03 Jan 2015 20:58:33 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 03 Jan 2015 20:51:10 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 03 Jan 2015 20:48:10 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 03 Jan 2015 20:44:08 +0100 |
wenzelm |
tuned menu items;
|
changeset |
files
|
| Sat, 03 Jan 2015 20:28:53 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 03 Jan 2015 20:22:27 +0100 |
wenzelm |
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
|
changeset |
files
|
| Sat, 03 Jan 2015 15:45:01 +0100 |
wenzelm |
more uniform support for graph display in ML/Scala;
|
changeset |
files
|
| Sat, 03 Jan 2015 14:54:33 +0100 |
wenzelm |
recovered tooltip from 6e77ddb1e3fb: non-null default is required as prerequisite;
|
changeset |
files
|
| Sat, 03 Jan 2015 14:29:07 +0100 |
wenzelm |
prefer integer coordinates;
|
changeset |
files
|
| Sat, 03 Jan 2015 13:11:10 +0100 |
wenzelm |
clarified bounding box, similar to old graph browser;
|
changeset |
files
|
| Fri, 02 Jan 2015 21:19:34 +0100 |
wenzelm |
tuned headers;
|
changeset |
files
|
| Fri, 02 Jan 2015 20:54:14 +0100 |
wenzelm |
less excessive event handling;
|
changeset |
files
|
| Fri, 02 Jan 2015 20:37:34 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 02 Jan 2015 20:13:48 +0100 |
wenzelm |
clarified mouse wheel: conventional scrolling, not scaling;
|
changeset |
files
|
| Fri, 02 Jan 2015 19:54:13 +0100 |
wenzelm |
clarified metrics, similar to old graph browser;
|
changeset |
files
|
| Thu, 01 Jan 2015 21:23:01 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 01 Jan 2015 21:19:36 +0100 |
wenzelm |
tuned color;
|
changeset |
files
|
| Thu, 01 Jan 2015 21:09:07 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 01 Jan 2015 21:01:18 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 01 Jan 2015 20:50:20 +0100 |
wenzelm |
more dynamic visualizer -- re-use jEdit font info;
|
changeset |
files
|
| Thu, 01 Jan 2015 17:27:52 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 01 Jan 2015 16:08:12 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 01 Jan 2015 15:58:30 +0100 |
wenzelm |
more dynamic visualizer -- re-use Isabelle/jEdit options;
|
changeset |
files
|
| Thu, 01 Jan 2015 14:53:57 +0100 |
wenzelm |
more standard GUI layout;
|
changeset |
files
|
| Thu, 01 Jan 2015 14:40:20 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 01 Jan 2015 14:37:25 +0100 |
wenzelm |
tuned imports;
|
changeset |
files
|
| Thu, 01 Jan 2015 14:21:26 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 01 Jan 2015 14:05:48 +0100 |
wenzelm |
tuned imports;
|
changeset |
files
|
| Thu, 01 Jan 2015 14:02:28 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 01 Jan 2015 13:07:30 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 01 Jan 2015 12:34:15 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 01 Jan 2015 12:20:22 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 01 Jan 2015 11:37:09 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Thu, 01 Jan 2015 11:12:15 +0100 |
boehmes |
merged
|
changeset |
files
|
| Thu, 01 Jan 2015 11:08:47 +0100 |
boehmes |
updated NEWS
|
changeset |
files
|
| Mon, 29 Dec 2014 22:14:13 +0100 |
boehmes |
optionally display statistics for Z3 proof reconstruction
|
changeset |
files
|
| Mon, 29 Dec 2014 16:21:33 +0100 |
boehmes |
avoid more than one data slot per module
|
changeset |
files
|
| Mon, 29 Dec 2014 14:57:13 +0100 |
boehmes |
limit reconstruction time of Z3 proof steps to be able to detect long-running reconstruction steps
|
changeset |
files
|
| Wed, 31 Dec 2014 21:45:30 +0100 |
wenzelm |
converse graph according to Graph_Display;
|
changeset |
files
|
| Wed, 31 Dec 2014 20:55:11 +0100 |
wenzelm |
eliminated TTY/PG legacy;
|
changeset |
files
|
| Wed, 31 Dec 2014 20:42:45 +0100 |
wenzelm |
clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names);
|
changeset |
files
|
| Wed, 31 Dec 2014 14:28:04 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 31 Dec 2014 14:15:52 +0100 |
wenzelm |
for graph display, prefer graph data structure over list with dependencies;
|
changeset |
files
|
| Wed, 31 Dec 2014 14:13:11 +0100 |
wenzelm |
more explict and generic field names
|
changeset |
files
|
| Wed, 31 Dec 2014 14:08:50 +0100 |
wenzelm |
uniform variable name for presentation graphs, to distinguish from values of type Graph.T
|
changeset |
files
|
| Wed, 31 Dec 2014 14:05:06 +0100 |
wenzelm |
stripped ad-hoc diagnostic facility
|
changeset |
files
|
| Wed, 31 Dec 2014 11:27:26 +1100 |
kleing |
update map definition in Prog_Prove for new datatype package
|
changeset |
files
|
| Tue, 30 Dec 2014 23:45:03 +0100 |
wenzelm |
explicit message channel for "legacy", which is nonetheless a variant of "warning";
|
changeset |
files
|
| Tue, 30 Dec 2014 14:11:06 +0100 |
wenzelm |
clarified source location;
|
changeset |
files
|
| Tue, 30 Dec 2014 11:50:34 +0100 |
wenzelm |
added system property isabelle.laf, notably for initial system dialog;
|
changeset |
files
|
| Tue, 30 Dec 2014 10:38:10 +0100 |
wenzelm |
NEWS;
|
changeset |
files
|
| Mon, 29 Dec 2014 21:02:49 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 29 Dec 2014 20:51:42 +0100 |
wenzelm |
clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
|
changeset |
files
|
| Mon, 29 Dec 2014 19:17:24 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Mon, 29 Dec 2014 15:38:59 +0100 |
wenzelm |
more toplevel pretty printing;
|
changeset |
files
|
| Sun, 28 Dec 2014 22:10:09 +0100 |
wenzelm |
back to full synchronization (cf. eb3e399f5b9f);
|
changeset |
files
|
| Sun, 28 Dec 2014 22:03:11 +0100 |
wenzelm |
proper sequential version;
|
changeset |
files
|
| Sun, 28 Dec 2014 21:34:45 +0100 |
wenzelm |
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
|
changeset |
files
|
| Sun, 28 Dec 2014 12:37:03 +0100 |
wenzelm |
modernized historic example;
|
changeset |
files
|
| Sun, 28 Dec 2014 12:18:01 +0100 |
wenzelm |
more thorough Lazy.is_finished;
|
changeset |
files
|
| Sun, 28 Dec 2014 15:42:34 +1100 |
kleing |
3 old example lemmas by Amine listed in the top 100 theorems
|
changeset |
files
|
| Sat, 27 Dec 2014 20:32:06 +0100 |
wenzelm |
update_cartouches;
|
changeset |
files
|
| Sat, 27 Dec 2014 19:51:55 +0100 |
wenzelm |
memo_fork without locking, to avoid rare deadlock in Event_Timer.request due to execution overrun;
|
changeset |
files
|
| Wed, 24 Dec 2014 10:06:37 +0100 |
haftmann |
typos
|
changeset |
files
|
| Tue, 23 Dec 2014 21:14:44 +0100 |
wenzelm |
unused;
|
changeset |
files
|
| Tue, 23 Dec 2014 21:04:53 +0100 |
wenzelm |
tuned message;
|
changeset |
files
|
| Tue, 23 Dec 2014 20:46:42 +0100 |
wenzelm |
explicit message channels for "state", "information";
|
changeset |
files
|
| Tue, 23 Dec 2014 16:00:38 +0100 |
wenzelm |
imitate font more carefully: err on smaller size;
|
changeset |
files
|
| Mon, 22 Dec 2014 21:34:11 +0100 |
wenzelm |
more accurate selection of sessions;
|
changeset |
files
|
| Mon, 22 Dec 2014 21:27:59 +0100 |
wenzelm |
more accurate selection of sessions;
|
changeset |
files
|
| Mon, 22 Dec 2014 20:40:37 +0100 |
wenzelm |
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
|
changeset |
files
|
| Mon, 22 Dec 2014 19:47:58 +0100 |
wenzelm |
more elementary Multithreading.synchronized;
|
changeset |
files
|
| Mon, 22 Dec 2014 18:10:54 +0100 |
wenzelm |
proper Synchronized.var;
|
changeset |
files
|
| Mon, 22 Dec 2014 17:17:00 +0100 |
wenzelm |
removed remains from Proof General;
|
changeset |
files
|
| Mon, 22 Dec 2014 16:44:54 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
| Mon, 22 Dec 2014 16:44:24 +0100 |
wenzelm |
system option "pretty_margin" is superseded by "thy_output_margin";
|
changeset |
files
|
| Mon, 22 Dec 2014 15:50:16 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 22 Dec 2014 14:35:42 +0100 |
wenzelm |
proper Synchronized.var;
|
changeset |
files
|
| Mon, 22 Dec 2014 14:33:53 +0100 |
wenzelm |
separate module Random;
|
changeset |
files
|
| Sun, 21 Dec 2014 22:49:40 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 21 Dec 2014 22:49:17 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 21 Dec 2014 19:14:16 +0100 |
wenzelm |
proper context;
|
changeset |
files
|
| Sun, 21 Dec 2014 16:27:22 +0100 |
wenzelm |
afford more heap;
|
changeset |
files
|
| Sun, 21 Dec 2014 16:26:22 +0100 |
wenzelm |
increase chances of success;
|
changeset |
files
|
| Sun, 21 Dec 2014 15:59:19 +0100 |
wenzelm |
recovered metis proof after 115965966e15 (Odd clash of type variables!?);
|
changeset |
files
|
| Sun, 21 Dec 2014 15:03:45 +0100 |
wenzelm |
proper context;
|
changeset |
files
|
| Sat, 20 Dec 2014 22:23:37 +0100 |
wenzelm |
proper context for "net" tactics;
|
changeset |
files
|
| Sat, 20 Dec 2014 19:12:41 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 20 Dec 2014 00:05:20 +0100 |
wenzelm |
afford full test, with slightly improved scheduling order;
|
changeset |
files
|
| Fri, 19 Dec 2014 23:33:08 +0100 |
wenzelm |
more generous timeout, to increase chances of at64-poly;
|
changeset |
files
|
| Fri, 19 Dec 2014 23:27:00 +0100 |
wenzelm |
updated according to eb3e399f5b9f;
|
changeset |
files
|
| Fri, 19 Dec 2014 23:01:46 +0100 |
wenzelm |
just one data slot per program unit;
|
changeset |
files
|
| Fri, 19 Dec 2014 22:53:43 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 19 Dec 2014 21:59:18 +0100 |
wenzelm |
just one data slot per program unit;
|
changeset |
files
|
| Fri, 19 Dec 2014 21:24:59 +0100 |
wenzelm |
more standard configuration options;
|
changeset |
files
|
| Fri, 19 Dec 2014 20:32:54 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 19 Dec 2014 20:10:59 +0100 |
wenzelm |
just one data slot per program unit;
|
changeset |
files
|
| Fri, 19 Dec 2014 20:09:31 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 19 Dec 2014 17:23:56 +0100 |
wenzelm |
more frugal Local_Syntax.init -- maintain idents within context;
|
changeset |
files
|
| Fri, 19 Dec 2014 12:56:06 +0100 |
wenzelm |
proper exception for internal program failure, not user-error;
|
changeset |
files
|
| Fri, 19 Dec 2014 12:36:50 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 18 Dec 2014 21:10:39 +0100 |
wenzelm |
suppress irrelevant timing messages (the majority);
|
changeset |
files
|
| Thu, 18 Dec 2014 17:26:53 +0100 |
wenzelm |
less ambitious settings -- increase chances of success;
|
changeset |
files
|
| Thu, 18 Dec 2014 16:13:54 +0100 |
wenzelm |
peek value without synchronization;
|
changeset |
files
|
| Thu, 18 Dec 2014 15:21:54 +0100 |
wenzelm |
avoid repeated access to global variable (101 times in Complex_Main), which is actually synchronized after e557a9ddee5f;
|
changeset |
files
|
| Wed, 17 Dec 2014 16:51:29 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 17 Dec 2014 16:10:30 +0100 |
hoelzl |
unfortunately, there is no general function space in the measurable spaces
|
changeset |
files
|
| Mon, 15 Dec 2014 07:20:49 +0100 |
blanchet |
correctly apply type substitution before checking for function types
|
changeset |
files
|
| Mon, 15 Dec 2014 07:20:48 +0100 |
blanchet |
avoid generating selectors with function types -- this produce arity inconsistencies
|
changeset |
files
|
| Mon, 15 Dec 2014 07:20:48 +0100 |
blanchet |
renamed theory file
|
changeset |
files
|
| Fri, 12 Dec 2014 14:42:37 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 12 Dec 2014 14:31:57 +0100 |
wenzelm |
Synchronized.value is actually synchronized (NB: underlying Unsynchronized.ref is not necessarily volatile);
|
changeset |
files
|
| Fri, 12 Dec 2014 14:30:33 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 11 Dec 2014 23:42:03 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 11 Dec 2014 23:31:30 +0100 |
wenzelm |
added Par_List in Scala, in accordance to ML version;
|
changeset |
files
|
| Thu, 11 Dec 2014 15:24:28 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 12 Dec 2014 10:58:40 +0100 |
hoelzl |
rel_pmf commutes with rel_prod
|
changeset |
files
|
| Thu, 11 Dec 2014 14:14:39 +0100 |
traytel |
note more facts (always)
|
changeset |
files
|
| Thu, 11 Dec 2014 14:14:18 +0100 |
traytel |
conceal typedef more violently
|
changeset |
files
|
| Thu, 11 Dec 2014 14:01:40 +0100 |
traytel |
respect order of deads when retrieving bnfs from the database
|
changeset |
files
|
| Wed, 10 Dec 2014 20:56:33 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 10 Dec 2014 20:51:27 +0100 |
wenzelm |
more informative gutter content: fall-back on background color, e.g. when line numbers are enabled;
|
changeset |
files
|
| Wed, 10 Dec 2014 19:26:01 +0100 |
wenzelm |
more examples;
|
changeset |
files
|
| Wed, 10 Dec 2014 19:24:54 +0100 |
wenzelm |
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
|
changeset |
files
|
| Wed, 10 Dec 2014 17:55:31 +0100 |
wenzelm |
more markup for improper situations;
|
changeset |
files
|
| Wed, 10 Dec 2014 13:45:44 +0100 |
wenzelm |
more explicit markup for improper commands;
|
changeset |
files
|
| Wed, 10 Dec 2014 10:44:56 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 09 Dec 2014 22:13:48 +0100 |
wenzelm |
imitate command markup and rendering of Isabelle/jEdit in HTML output;
|
changeset |
files
|
| Tue, 09 Dec 2014 21:14:11 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 09 Dec 2014 20:00:45 +0100 |
wenzelm |
more jEdit colors;
|
changeset |
files
|
| Tue, 09 Dec 2014 19:52:26 +0100 |
wenzelm |
proper alt_string markup (cf. 2ceb05ee0331);
|
changeset |
files
|
| Tue, 09 Dec 2014 19:39:40 +0100 |
wenzelm |
tuned spelling;
|
changeset |
files
|
| Tue, 09 Dec 2014 19:01:07 +0100 |
wenzelm |
clarified language context, e.g. relevant for symbol completion within cartouches;
|
changeset |
files
|
| Tue, 09 Dec 2014 18:29:45 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 09 Dec 2014 17:40:42 +0100 |
wenzelm |
proper railsetup;
|
changeset |
files
|
| Tue, 09 Dec 2014 16:22:40 +0100 |
hoelzl |
move topology on enat to Extended_Real, otherwise Jinja_Threads fails
|
changeset |
files
|
| Sat, 22 Nov 2014 11:05:41 +0100 |
wenzelm |
isatest for Mac OS X Yosemite;
|
changeset |
files
|
| Mon, 08 Dec 2014 23:06:19 +0100 |
wenzelm |
tuned spelling;
|
changeset |
files
|
| Mon, 08 Dec 2014 22:42:12 +0100 |
wenzelm |
expand ML cartouches to Input.source;
|
changeset |
files
|
| Mon, 08 Dec 2014 16:04:50 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 08 Dec 2014 15:59:30 +0100 |
wenzelm |
some special cases for official SML, to treat Isabelle symbols like raw characters;
|
changeset |
files
|
| Mon, 08 Dec 2014 15:21:57 +0100 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Mon, 08 Dec 2014 11:50:04 +0100 |
wenzelm |
clarified Isabelle/ML strings (refining 72238ea2201c);
|
changeset |
files
|
| Mon, 08 Dec 2014 11:49:04 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 08 Dec 2014 14:32:11 +0100 |
hoelzl |
instance bool and enat as topologies
|
changeset |
files
|
| Mon, 08 Dec 2014 12:30:47 +0100 |
haftmann |
NEWS
|
changeset |
files
|
| Fri, 05 Dec 2014 19:35:36 +0100 |
haftmann |
allow multiple inheritance of targets
|
changeset |
files
|
| Thu, 04 Dec 2014 16:51:54 +0100 |
haftmann |
tuned module structure
|
changeset |
files
|
| Thu, 04 Dec 2014 16:51:54 +0100 |
haftmann |
tuned data structures
|
changeset |
files
|
| Thu, 04 Dec 2014 16:51:54 +0100 |
haftmann |
tuned target inheritance bookkeeping: ancestry is always fully maintained at current entry using canonical merge;
|
changeset |
files
|
| Thu, 04 Dec 2014 16:51:54 +0100 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 04 Dec 2014 16:51:54 +0100 |
haftmann |
tuned names
|
changeset |
files
|
| Thu, 04 Dec 2014 16:51:54 +0100 |
haftmann |
eta-expand all search patterns using schematic place holders
|
changeset |
files
|
| Thu, 04 Dec 2014 16:51:54 +0100 |
haftmann |
revert "better" handling of abbreviation from c61fe520602b
|
changeset |
files
|
| Thu, 04 Dec 2014 16:51:54 +0100 |
haftmann |
tuned variable names
|
changeset |
files
|
| Thu, 04 Dec 2014 16:51:54 +0100 |
haftmann |
turn application-specific Pattern.matches_subterm into an application-private function
|
changeset |
files
|
| Thu, 04 Dec 2014 16:51:54 +0100 |
haftmann |
cleaned up mess
|
changeset |
files
|
| Fri, 05 Dec 2014 13:39:59 +0100 |
hoelzl |
add Poisson and Binomial distribution
|
changeset |
files
|
| Fri, 05 Dec 2014 12:06:18 +0100 |
hoelzl |
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
|
changeset |
files
|
| Thu, 04 Dec 2014 21:28:35 +0100 |
wenzelm |
proper GUI_Thread context (cf. 7e0d3da6e6d8);
|
changeset |
files
|
| Thu, 04 Dec 2014 20:56:38 +0100 |
wenzelm |
more examples;
|
changeset |
files
|
| Thu, 04 Dec 2014 20:45:11 +0100 |
wenzelm |
tuned header;
|
changeset |
files
|
| Thu, 04 Dec 2014 17:05:58 +0100 |
hoelzl |
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
|
changeset |
files
|
| Wed, 03 Dec 2014 22:44:24 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 03 Dec 2014 22:34:28 +0100 |
wenzelm |
node-specific keywords, with session base syntax as default;
|
changeset |
files
|
| Wed, 03 Dec 2014 20:45:20 +0100 |
wenzelm |
clarified define_command: send tokens more directly, without requiring keywords in ML;
|
changeset |
files
|
| Wed, 03 Dec 2014 15:22:27 +0100 |
wenzelm |
more robust bundle_name: avoid assumptions about identifier, keywords etc.;
|
changeset |
files
|
| Wed, 03 Dec 2014 14:04:38 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 03 Dec 2014 11:50:58 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 03 Dec 2014 11:37:51 +0100 |
wenzelm |
clarified token kind;
|
changeset |
files
|
| Tue, 02 Dec 2014 17:30:53 +0100 |
wenzelm |
added Untyped.method convenience (for *this* class only);
|
changeset |
files
|
| Tue, 02 Dec 2014 16:40:11 +0100 |
wenzelm |
tuned signature -- more explicit types;
|
changeset |
files
|
| Tue, 02 Dec 2014 16:10:11 +0100 |
wenzelm |
more careful syntax_changed propagation -- avoid global jEdit.propertiesChanged;
|
changeset |
files
|
| Tue, 02 Dec 2014 14:16:56 +0100 |
wenzelm |
node-specific syntax, with base_syntax as default;
|
changeset |
files
|
| Mon, 01 Dec 2014 19:25:20 +0100 |
wenzelm |
clarified token marker / syntax for mode vs. buffer;
|
changeset |
files
|
| Mon, 01 Dec 2014 17:51:07 +0100 |
wenzelm |
Sidekick syntax is derived from buffer (and its mode), instead of parser name;
|
changeset |
files
|
| Mon, 01 Dec 2014 17:43:23 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 01 Dec 2014 15:21:49 +0100 |
wenzelm |
more merge operations;
|
changeset |
files
|
| Mon, 01 Dec 2014 14:24:05 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 01 Dec 2014 13:49:47 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 03 Dec 2014 17:08:24 +0100 |
blanchet |
prefer E 1.8, now that it's been tried and tested
|
changeset |
files
|
| Sun, 30 Nov 2014 15:11:50 +0100 |
wenzelm |
more accurate context;
|
changeset |
files
|
| Sun, 30 Nov 2014 14:43:00 +0100 |
wenzelm |
update_cartouches;
|
changeset |
files
|
| Sun, 30 Nov 2014 14:02:48 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 30 Nov 2014 13:15:04 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 30 Nov 2014 12:46:16 +0100 |
wenzelm |
tuned signature -- prefer Input.source;
|
changeset |
files
|
| Sun, 30 Nov 2014 12:24:56 +0100 |
wenzelm |
more abstract type Input.source;
|
changeset |
files
|
| Sat, 29 Nov 2014 14:43:10 +0100 |
wenzelm |
encode text with control symbols;
|
changeset |
files
|
| Sat, 29 Nov 2014 14:42:32 +0100 |
wenzelm |
proper HTML.encode;
|
changeset |
files
|
| Wed, 26 Nov 2014 15:59:46 +0100 |
haftmann |
prefer abbrev for is_unit
|
changeset |
files
|
| Wed, 26 Nov 2014 15:46:19 +0100 |
haftmann |
do not conceal inductive predicate names properly, following 4a3747517552
|
changeset |
files
|
| Wed, 26 Nov 2014 15:46:17 +0100 |
haftmann |
tuned
|
changeset |
files
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
changeset |
files
|
| Wed, 26 Nov 2014 16:55:43 +0100 |
wenzelm |
added ML antiquotation @{apply n} or @{apply n(k)};
|
changeset |
files
|
| Wed, 26 Nov 2014 15:44:32 +0100 |
wenzelm |
even more exception traces for Document.update, which goes through additional execution wrappers;
|
changeset |
files
|
| Wed, 26 Nov 2014 14:35:55 +0100 |
wenzelm |
more informative failure of protocol commands, with exception trace;
|
changeset |
files
|
| Wed, 26 Nov 2014 11:43:51 +0100 |
wenzelm |
load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
|
changeset |
files
|
| Tue, 25 Nov 2014 17:30:05 +0100 |
hoelzl |
tuned proof that pmfs are bnfs
|
changeset |
files
|
| Tue, 25 Nov 2014 17:29:39 +0100 |
hoelzl |
projections of pair_pmf (by D. Traytel)
|
changeset |
files
|
| Mon, 24 Nov 2014 22:59:20 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 24 Nov 2014 20:06:51 +0100 |
wenzelm |
removed odd remains of structural containment checks, which stem from an older approach (see also 3ad1b289f21b, 3ae3cc4b1eac, 423af2e013b8, bad13b32c0f3, ccd6de95f4a6);
|
changeset |
files
|
| Mon, 24 Nov 2014 15:50:10 +0100 |
traytel |
preinstantiate (co)inductions in N2M to handle mutual but separated SCCs
|
changeset |
files
|
| Mon, 24 Nov 2014 12:20:14 +0100 |
hoelzl |
add congruence solver to measurability prover
|
changeset |
files
|
| Mon, 24 Nov 2014 12:20:35 +0100 |
hoelzl |
cleanup measurability prover
|
changeset |
files
|
| Mon, 24 Nov 2014 12:35:13 +0100 |
blanchet |
updated SMT certificates
|
changeset |
files
|
| Mon, 24 Nov 2014 12:35:13 +0100 |
blanchet |
added one more CVC4 option that helps Judgment Day (10 theory version)
|
changeset |
files
|
| Mon, 24 Nov 2014 12:35:13 +0100 |
blanchet |
tuned whitespace
|
changeset |
files
|
| Mon, 24 Nov 2014 12:35:13 +0100 |
blanchet |
keep all 'ctr' theorems
|
changeset |
files
|
| Mon, 24 Nov 2014 12:35:13 +0100 |
blanchet |
smoothly handle unit codatatypes in 'primcorec'
|
changeset |
files
|
| Mon, 24 Nov 2014 12:35:13 +0100 |
blanchet |
careful with de Bruijn indices
|
changeset |
files
|
| Mon, 24 Nov 2014 12:35:13 +0100 |
blanchet |
improved message in 'co' case
|
changeset |
files
|
| Mon, 24 Nov 2014 12:35:13 +0100 |
blanchet |
updated NEWS
|
changeset |
files
|
| Mon, 24 Nov 2014 12:35:13 +0100 |
blanchet |
no need for subset operation as a primitive in Nitpick, esp. that its implementation was unsound (cf. Rene Thiemann's 16 Oct 2014 email on isabelle mailing list)
|
changeset |
files
|
| Mon, 24 Nov 2014 12:35:13 +0100 |
blanchet |
added Z3 reconstruction rule suggested by F. Maric
|
changeset |
files
|
| Mon, 24 Nov 2014 12:35:13 +0100 |
blanchet |
one more CVC4 option that helps
|
changeset |
files
|
| Mon, 24 Nov 2014 12:35:13 +0100 |
blanchet |
renamed 'veriT' to 'verit', to stick to all-lowercase rule for prover names
|
changeset |
files
|
| Mon, 24 Nov 2014 12:35:13 +0100 |
blanchet |
update CVC4 version docs
|
changeset |
files
|
| Sat, 22 Nov 2014 15:34:00 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 22 Nov 2014 15:27:48 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 22 Nov 2014 14:57:04 +0100 |
wenzelm |
misc tuning and modernization;
|
changeset |
files
|
| Sat, 22 Nov 2014 14:13:36 +0100 |
wenzelm |
misc tuning and modernization;
|
changeset |
files
|
| Sat, 22 Nov 2014 13:38:15 +0100 |
wenzelm |
more careful ML source positions, for improved PIDE markup;
|
changeset |
files
|
| Sat, 22 Nov 2014 11:36:00 +0100 |
wenzelm |
named_theorems: multiple args;
|
changeset |
files
|
| Fri, 21 Nov 2014 22:59:32 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 21 Nov 2014 18:14:39 +0100 |
wenzelm |
removed some add-ons from modules that are relevant for the inference kernel;
|
changeset |
files
|
| Fri, 21 Nov 2014 13:18:56 +0100 |
Andreas Lochbihler |
add lemma following a proof suggestion by Joachim Breitner
|
changeset |
files
|
| Fri, 21 Nov 2014 12:24:59 +0100 |
Andreas Lochbihler |
add lemma
|
changeset |
files
|
| Fri, 21 Nov 2014 12:11:44 +0100 |
Andreas Lochbihler |
register pmf as BNF
|
changeset |
files
|
| Thu, 20 Nov 2014 17:29:18 +0100 |
blanchet |
added CVC4 option that helps on JD
|
changeset |
files
|
| Thu, 20 Nov 2014 17:29:18 +0100 |
blanchet |
always generate patterns as lists of lists, to avoid confusing CVC4 (and stick to what SMT-LIB 2 actually says)
|
changeset |
files
|
| Thu, 20 Nov 2014 17:29:18 +0100 |
blanchet |
work around bug in CVC4, with boolean arguments to (co)datatypes
|
changeset |
files
|
| Thu, 20 Nov 2014 17:29:18 +0100 |
blanchet |
other way of crashing (with CVC4)
|
changeset |
files
|
| Thu, 20 Nov 2014 17:29:18 +0100 |
blanchet |
set right logic for CVC4 with (co)datatypes
|
changeset |
files
|
| Thu, 20 Nov 2014 17:29:18 +0100 |
blanchet |
removed explicit '--quant-cf' option to CVC4, now that it's the default
|
changeset |
files
|
| Wed, 19 Nov 2014 19:12:14 +0100 |
traytel |
more accurate lemma name
|
changeset |
files
|
| Wed, 19 Nov 2014 10:31:15 +0100 |
blanchet |
parse CVC4 unsat cores
|
changeset |
files
|
| Wed, 19 Nov 2014 10:31:15 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 19 Nov 2014 10:31:15 +0100 |
blanchet |
removed redundant code line
|
changeset |
files
|
| Tue, 18 Nov 2014 20:56:34 +0100 |
wenzelm |
clarified Table.make_set: duplicate arguments are allowed, like Table.make_list or Scala Set() formation;
|
changeset |
files
|
| Mon, 17 Nov 2014 18:19:06 +0100 |
hoelzl |
add reindex rules for distr and nn_integral on count_space
|
changeset |
files
|
| Mon, 17 Nov 2014 14:55:34 +0100 |
haftmann |
generalized lemmas and tuned proofs
|
changeset |
files
|
| Mon, 17 Nov 2014 14:55:33 +0100 |
haftmann |
generalized lemmas (particularly concerning dvd) as far as appropriate
|
changeset |
files
|
| Mon, 17 Nov 2014 14:55:32 +0100 |
haftmann |
formally self-contained gcd type classes
|
changeset |
files
|
| Fri, 14 Nov 2014 22:13:45 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 14 Nov 2014 21:36:50 +0100 |
wenzelm |
no quick_and_dirty for proof extraction, to avoid obscure errors like "corr: bad proof";
|
changeset |
files
|
| Fri, 14 Nov 2014 17:07:06 +0100 |
wenzelm |
use \isastyletext directly via 'text' command;
|
changeset |
files
|
| Fri, 14 Nov 2014 11:19:14 +0100 |
wenzelm |
proper sequential version (cf. 302104d8366b);
|
changeset |
files
|
| Fri, 14 Nov 2014 18:39:42 +0100 |
haftmann |
documentation stubs about permanent_interpretation
|
changeset |
files
|
| Fri, 14 Nov 2014 13:18:33 +0100 |
hoelzl |
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
|
changeset |
files
|
| Fri, 14 Nov 2014 08:18:58 +0100 |
hoelzl |
merged
|
changeset |
files
|
| Thu, 13 Nov 2014 17:19:52 +0100 |
hoelzl |
import general theorems from AFP/Markov_Models
|
changeset |
files
|
| Thu, 13 Nov 2014 23:45:15 +0100 |
wenzelm |
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
|
changeset |
files
|
| Thu, 13 Nov 2014 17:28:11 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 13 Nov 2014 14:40:06 +0100 |
traytel |
merged
|
changeset |
files
|
| Thu, 13 Nov 2014 14:14:13 +0100 |
traytel |
do not introduce consts too early unnecessarily
|
changeset |
files
|
| Thu, 13 Nov 2014 12:35:55 +0100 |
nipkow |
added lemma
|
changeset |
files
|
| Wed, 12 Nov 2014 19:30:56 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 12 Nov 2014 18:18:38 +0100 |
wenzelm |
prefer independent parallel map where user input is processed -- avoid non-deterministic feedback in error situations;
|
changeset |
files
|
| Wed, 12 Nov 2014 11:39:27 +0100 |
wenzelm |
make SML/NJ happy;
|
changeset |
files
|
| Wed, 12 Nov 2014 10:30:59 +0100 |
wenzelm |
more careful ML source positions, for improved PIDE markup;
|
changeset |
files
|
| Wed, 12 Nov 2014 17:37:44 +0100 |
immler |
NEWS
|
changeset |
files
|
| Wed, 12 Nov 2014 17:37:43 +0100 |
immler |
tuned proofs
|
changeset |
files
|
| Wed, 12 Nov 2014 17:37:43 +0100 |
immler |
added quickcheck[approximation]
|
changeset |
files
|
| Wed, 12 Nov 2014 17:37:43 +0100 |
immler |
quickcheck setup for float, inspired by rat::{exhaustive,full_exhaustive,random}
|
changeset |
files
|
| Wed, 12 Nov 2014 17:37:43 +0100 |
immler |
disjunction and conjunction for forms
|
changeset |
files
|
| Wed, 12 Nov 2014 17:37:43 +0100 |
immler |
truncate intermediate results in horner to improve performance of approximate;
|
changeset |
files
|
| Wed, 12 Nov 2014 17:36:36 +0100 |
immler |
added lemmas: convert between powr and log in comparisons, pull log out of addition/subtraction
|
changeset |
files
|
| Wed, 12 Nov 2014 17:36:32 +0100 |
immler |
cancel real of power of numeral also for equality and strict inequality;
|
changeset |
files
|
| Wed, 12 Nov 2014 17:36:29 +0100 |
immler |
simplified computations based on round_up by reducing to round_down;
|
changeset |
files
|
| Wed, 12 Nov 2014 17:36:25 +0100 |
immler |
code equation for powr
|
changeset |
files
|
| Tue, 11 Nov 2014 21:14:19 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 11 Nov 2014 20:11:38 +0100 |
wenzelm |
more careful ML source positions, for improved PIDE markup;
|
changeset |
files
|
| Tue, 11 Nov 2014 18:16:25 +0100 |
wenzelm |
more position information, e.g. relevant for errors in generated ML source;
|
changeset |
files
|
| Tue, 11 Nov 2014 15:55:31 +0100 |
wenzelm |
more symbols;
|
changeset |
files
|
| Tue, 11 Nov 2014 13:50:56 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Tue, 11 Nov 2014 13:44:09 +0100 |
wenzelm |
more markup;
|
changeset |
files
|
| Tue, 11 Nov 2014 13:40:13 +0100 |
wenzelm |
simplifie sessions;
|
changeset |
files
|
| Tue, 11 Nov 2014 11:47:53 +0100 |
wenzelm |
more Isar proof methods;
|
changeset |
files
|
| Tue, 11 Nov 2014 11:41:58 +0100 |
wenzelm |
more Isar proof methods;
|
changeset |
files
|
| Tue, 11 Nov 2014 10:54:52 +0100 |
wenzelm |
more Isar proof methods;
|
changeset |
files
|
| Tue, 11 Nov 2014 19:38:45 +0100 |
noschinl |
add forgotten lemma
|
changeset |
files
|
| Tue, 11 Nov 2014 14:46:26 +0100 |
noschinl |
added lemma
|
changeset |
files
|
| Tue, 11 Nov 2014 12:30:37 +0100 |
desharna |
make 'corec_transfer' tactic more robust
|
changeset |
files
|
| Tue, 11 Nov 2014 12:30:36 +0100 |
desharna |
also generate '(co)rec_transfer' for (co)datatypes with 0 live type variables
|
changeset |
files
|
| Tue, 11 Nov 2014 10:26:08 +0100 |
desharna |
make 'rec_transfer' tactic more robust
|
changeset |
files
|
| Tue, 11 Nov 2014 08:57:46 +0100 |
Andreas Lochbihler |
add del option to measurable;
|
changeset |
files
|
| Tue, 11 Nov 2014 00:11:11 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 10 Nov 2014 21:49:48 +0100 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
changeset |
files
|
| Mon, 10 Nov 2014 15:09:58 +0100 |
nipkow |
even -> evn because even is now in Main
|
changeset |
files
|
| Mon, 10 Nov 2014 10:29:19 +0100 |
traytel |
dropped redundant transfer rules (now proved and registered by datatype and plugins)
|
changeset |
files
|
| Sun, 09 Nov 2014 20:49:28 +0100 |
wenzelm |
proper context for typedef;
|
changeset |
files
|
| Sun, 09 Nov 2014 20:41:53 +0100 |
wenzelm |
proper proof context for typedef;
|
changeset |
files
|
| Sun, 09 Nov 2014 18:27:43 +0100 |
wenzelm |
proper context;
|
changeset |
files
|
| Sun, 09 Nov 2014 17:04:14 +0100 |
wenzelm |
proper context for match_tac etc.;
|
changeset |
files
|
| Sun, 09 Nov 2014 14:08:00 +0100 |
wenzelm |
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
|
changeset |
files
|
| Sun, 09 Nov 2014 11:05:20 +0100 |
nipkow |
avoid erule and rotated in IMP
|
changeset |
files
|
| Sun, 09 Nov 2014 10:03:18 +0100 |
haftmann |
reverted 1ebf0a1f12a4 after successful re-tuning of simp rules for divisibility
|
changeset |
files
|
| Sun, 09 Nov 2014 10:03:17 +0100 |
haftmann |
self-contained simp rules for dvd on numerals
|
changeset |
files
|
| Sat, 08 Nov 2014 16:53:26 +0100 |
haftmann |
equivalence rules for structures without zero divisors
|
changeset |
files
|
| Sat, 08 Nov 2014 22:10:16 +0100 |
wenzelm |
removed obsolete global-only options, which did not work out anyway (due to complexity of local_theory sandwich);
|
changeset |
files
|
| Sat, 08 Nov 2014 21:31:51 +0100 |
wenzelm |
optional proof context for unify operations, for the sake of proper local options;
|
changeset |
files
|
| Sat, 08 Nov 2014 17:39:01 +0100 |
wenzelm |
clarified name of Type.unified, to emphasize its connection to the "unify" family;
|
changeset |
files
|
| Sat, 08 Nov 2014 16:55:41 +0100 |
wenzelm |
proper Envir.norm_type for result of Type.raw_unifys;
|
changeset |
files
|
| Sat, 08 Nov 2014 16:42:04 +0100 |
wenzelm |
avoid slow metis proof;
|
changeset |
files
|
| Sat, 08 Nov 2014 16:35:24 +0100 |
wenzelm |
proper Envir.norm_type for result of Unify.unifiers (amending 479832ff2d29 from 20 years ago);
|
changeset |
files
|
| Sat, 08 Nov 2014 15:45:00 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 08 Nov 2014 15:44:41 +0100 |
wenzelm |
updated some sledgehammer proofs -- much faster;
|
changeset |
files
|
| Sat, 08 Nov 2014 15:40:29 +0100 |
wenzelm |
updated sledgehammer proof after breakdown of metis (exception Type.TUNIFY);
|
changeset |
files
|
| Sat, 08 Nov 2014 15:01:05 +0100 |
wenzelm |
recovered type matching, which was broken in 8a765db7e0f8 (see also 8a765db7e0f8, 2db1d3d2ed54);
|
changeset |
files
|
| Sat, 08 Nov 2014 12:15:40 +0100 |
wenzelm |
more direct type equality;
|
changeset |
files
|
| Sat, 08 Nov 2014 09:19:57 +0100 |
haftmann |
reverted commit accident from 994fe0ba8335
|
changeset |
files
|
| Sat, 08 Nov 2014 09:16:47 +0100 |
haftmann |
less space-wasting serialization setup: highest cell of array has been unused so far
|
changeset |
files
|
| Fri, 07 Nov 2014 23:35:13 +0100 |
wenzelm |
tuned outline;
|
changeset |
files
|
| Fri, 07 Nov 2014 22:33:54 +0100 |
wenzelm |
tuned syntax -- separate tokens;
|
changeset |
files
|
| Fri, 07 Nov 2014 22:15:51 +0100 |
wenzelm |
eliminated pointless check -- command definitions are subject to theory context;
|
changeset |
files
|
| Fri, 07 Nov 2014 20:43:13 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 07 Nov 2014 20:06:18 +0100 |
wenzelm |
prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors;
|
changeset |
files
|
| Fri, 07 Nov 2014 19:47:05 +0100 |
wenzelm |
tuned markup;
|
changeset |
files
|
| Fri, 07 Nov 2014 17:43:50 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 07 Nov 2014 17:31:01 +0100 |
wenzelm |
clarified keyword categories;
|
changeset |
files
|
| Fri, 07 Nov 2014 16:55:09 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 07 Nov 2014 16:51:36 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 07 Nov 2014 16:36:55 +0100 |
wenzelm |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
|
changeset |
files
|
| Fri, 07 Nov 2014 16:22:25 +0100 |
wenzelm |
proper import for command 'permanent_interpretation';
|
changeset |
files
|
| Fri, 07 Nov 2014 16:13:05 +0100 |
wenzelm |
proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined *after* theory List;
|
changeset |
files
|
| Fri, 07 Nov 2014 15:19:30 +0100 |
wenzelm |
more accurate keywords;
|
changeset |
files
|
| Thu, 06 Nov 2014 16:10:33 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 06 Nov 2014 15:47:04 +0100 |
wenzelm |
more explicit Keyword.keywords;
|
changeset |
files
|
| Thu, 06 Nov 2014 15:42:34 +0100 |
wenzelm |
proper Keyword.keywords (cf. 82a71046dce8);
|
changeset |
files
|
| Thu, 06 Nov 2014 15:05:15 +0100 |
wenzelm |
prefer explicit Keyword.keywords (cf. 82a71046dce8);
|
changeset |
files
|
| Thu, 06 Nov 2014 13:44:14 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 06 Nov 2014 13:36:19 +0100 |
wenzelm |
prefer explicit Keyword.keywords;
|
changeset |
files
|
| Thu, 06 Nov 2014 11:44:41 +0100 |
wenzelm |
simplified keyword kinds;
|
changeset |
files
|
| Fri, 07 Nov 2014 15:40:08 +0000 |
paulson |
Tidying up. Removing unnecessary conditions from some theorems.
|
changeset |
files
|
| Fri, 07 Nov 2014 11:28:37 +0100 |
traytel |
more complete fp_sugars for sum and prod;
|
changeset |
files
|
| Fri, 07 Nov 2014 12:24:56 +0100 |
desharna |
document '*_transfer' attribute
|
changeset |
files
|
| Fri, 07 Nov 2014 11:52:56 +0100 |
desharna |
document 'size_neq'
|
changeset |
files
|
| Fri, 07 Nov 2014 11:52:54 +0100 |
desharna |
generate 'size_neq' for datatypes
|
changeset |
files
|
| Thu, 06 Nov 2014 15:21:59 +0100 |
desharna |
fix 'unfla' function
|
changeset |
files
|
| Wed, 05 Nov 2014 20:59:24 +0100 |
haftmann |
proper oriented equivalence of dvd predicate and mod
|
changeset |
files
|
| Wed, 05 Nov 2014 22:39:49 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 05 Nov 2014 22:37:14 +0100 |
wenzelm |
more symbols;
|
changeset |
files
|
| Wed, 05 Nov 2014 22:17:05 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 05 Nov 2014 21:59:21 +0100 |
wenzelm |
more uniform header_keywords in ML/Scala;
|
changeset |
files
|
| Wed, 05 Nov 2014 21:21:15 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 05 Nov 2014 21:10:38 +0100 |
wenzelm |
more frugal keywords;
|
changeset |
files
|
| Wed, 05 Nov 2014 20:49:30 +0100 |
wenzelm |
eliminated pointless dynamic keywords (TTY legacy);
|
changeset |
files
|
| Wed, 05 Nov 2014 20:20:57 +0100 |
wenzelm |
explicit type Keyword.keywords;
|
changeset |
files
|
| Wed, 05 Nov 2014 20:05:32 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 05 Nov 2014 17:37:25 +0100 |
wenzelm |
clarified representation of type Keywords;
|
changeset |
files
|
| Wed, 05 Nov 2014 16:57:12 +0100 |
wenzelm |
explicit type Keyword.Keywords;
|
changeset |
files
|
| Wed, 05 Nov 2014 15:32:11 +0100 |
wenzelm |
clarified minor/major lexicon (like ML version);
|
changeset |
files
|
| Wed, 05 Nov 2014 19:43:17 +0100 |
nipkow |
reduced execution time
|
changeset |
files
|
| Tue, 04 Nov 2014 18:19:38 +0100 |
wenzelm |
proper button margins for Nimbus L&F;
|
changeset |
files
|
| Tue, 04 Nov 2014 17:37:15 +0100 |
wenzelm |
approximative update of versions;
|
changeset |
files
|
| Tue, 04 Nov 2014 17:33:08 +0100 |
lammich |
Added Option.bind_split{,_asm,s}
|
changeset |
files
|
| Mon, 03 Nov 2014 15:08:15 +0100 |
wenzelm |
clarified legacy code;
|
changeset |
files
|
| Mon, 03 Nov 2014 14:50:27 +0100 |
wenzelm |
eliminated unused int_only flag (see also c12484a27367);
|
changeset |
files
|
| Mon, 03 Nov 2014 14:31:15 +0100 |
wenzelm |
eliminated obsolete Proof.goal_message -- print outcome more directly;
|
changeset |
files
|
| Mon, 03 Nov 2014 09:25:23 +0100 |
wenzelm |
updated to scala-2.11.4;
|
changeset |
files
|
| Sun, 02 Nov 2014 23:13:31 +0100 |
wenzelm |
less ambitious isatest: polyml-5.3.0 has problems with big sessions like HOL-Proofs;
|
changeset |
files
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
changeset |
files
|
| Sun, 02 Nov 2014 18:21:14 +0100 |
wenzelm |
prefer \setisabellecontext;
|
changeset |
files
|
| Sun, 02 Nov 2014 18:16:19 +0100 |
wenzelm |
modernized header;
|
changeset |
files
|
| Sun, 02 Nov 2014 17:58:35 +0100 |
wenzelm |
modernized header;
|
changeset |
files
|
| Sun, 02 Nov 2014 17:39:52 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
| Sun, 02 Nov 2014 17:36:52 +0100 |
wenzelm |
modernized header;
|
changeset |
files
|
| Sun, 02 Nov 2014 17:27:22 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
| Sun, 02 Nov 2014 17:23:48 +0100 |
wenzelm |
modernized header;
|
changeset |
files
|
| Sun, 02 Nov 2014 17:20:45 +0100 |
wenzelm |
modernized header;
|
changeset |
files
|
| Sun, 02 Nov 2014 17:16:01 +0100 |
wenzelm |
modernized header;
|
changeset |
files
|
| Sun, 02 Nov 2014 17:14:15 +0100 |
wenzelm |
modernized header;
|
changeset |
files
|
| Sun, 02 Nov 2014 17:13:28 +0100 |
wenzelm |
modernized header;
|
changeset |
files
|
| Sun, 02 Nov 2014 17:09:04 +0100 |
wenzelm |
modernized header;
|
changeset |
files
|
| Sun, 02 Nov 2014 17:06:05 +0100 |
wenzelm |
modernized header;
|
changeset |
files
|
| Sun, 02 Nov 2014 16:59:40 +0100 |
wenzelm |
clarified legacy command;
|
changeset |
files
|
| Sun, 02 Nov 2014 16:54:06 +0100 |
wenzelm |
modernized header;
|
changeset |
files
|
| Sun, 02 Nov 2014 16:50:42 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
| Sun, 02 Nov 2014 16:47:45 +0100 |
wenzelm |
added update_header tool;
|
changeset |
files
|
| Sun, 02 Nov 2014 16:39:54 +0100 |
wenzelm |
modernized header;
|
changeset |
files
|
| Sun, 02 Nov 2014 16:09:35 +0100 |
wenzelm |
more flexibile \setisabellecontext, independently of header;
|
changeset |
files
|
| Sun, 02 Nov 2014 16:05:43 +0100 |
wenzelm |
prefer explicit heading command;
|
changeset |
files
|
| Sun, 02 Nov 2014 15:27:37 +0100 |
wenzelm |
uniform heading commands work in any context, even in theory header;
|
changeset |
files
|
| Sun, 02 Nov 2014 13:26:20 +0100 |
wenzelm |
eliminated dead code;
|
changeset |
files
|
| Sat, 01 Nov 2014 20:19:07 +0100 |
wenzelm |
clarified syntax -- avoid overlap with command category;
|
changeset |
files
|
| Sat, 01 Nov 2014 19:47:48 +0100 |
wenzelm |
tuned signature (see ab2483fad861);
|
changeset |
files
|
| Sat, 01 Nov 2014 19:33:51 +0100 |
wenzelm |
recover via scanner;
|
changeset |
files
|
| Sat, 01 Nov 2014 18:46:48 +0100 |
wenzelm |
simplified -- scanning is never interactive;
|
changeset |
files
|
| Sat, 01 Nov 2014 15:35:40 +0100 |
wenzelm |
tuned signature, in accordance to Scala version;
|
changeset |
files
|
| Sat, 01 Nov 2014 15:01:41 +0100 |
wenzelm |
command-line terminator ";" is no longer accepted;
|
changeset |
files
|
| Sat, 01 Nov 2014 14:20:38 +0100 |
wenzelm |
eliminated spurious semicolons;
|
changeset |
files
|
| Sat, 01 Nov 2014 11:40:55 +0100 |
wenzelm |
eliminated former Proof General preferences;
|
changeset |
files
|
| Fri, 31 Oct 2014 23:51:54 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 31 Oct 2014 22:48:00 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 31 Oct 2014 22:37:22 +0100 |
wenzelm |
provide explicit theory (amending 621c052789b4);
|
changeset |
files
|
| Fri, 31 Oct 2014 22:09:18 +0100 |
wenzelm |
removed pointless markup;
|
changeset |
files
|
| Fri, 31 Oct 2014 22:02:49 +0100 |
wenzelm |
discontinued obsolete \<^sync> marker;
|
changeset |
files
|
| Fri, 31 Oct 2014 21:48:40 +0100 |
wenzelm |
discontinued obsolete control command category;
|
changeset |
files
|
| Fri, 31 Oct 2014 21:35:11 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
| Fri, 31 Oct 2014 21:20:06 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
| Fri, 31 Oct 2014 21:10:11 +0100 |
wenzelm |
discontinued obsolete tty and prompt;
|
changeset |
files
|
| Fri, 31 Oct 2014 18:56:59 +0100 |
wenzelm |
discontinued pointless option: timing is always on (overall theory only);
|
changeset |
files
|
| Fri, 31 Oct 2014 17:08:54 +0100 |
wenzelm |
eliminated odd flags and hook;
|
changeset |
files
|
| Fri, 31 Oct 2014 16:56:23 +0100 |
wenzelm |
avoid noise (cf. 03ff4d1e6784);
|
changeset |
files
|
| Fri, 31 Oct 2014 16:03:45 +0100 |
wenzelm |
discontinued Isar TTY loop;
|
changeset |
files
|
| Fri, 31 Oct 2014 15:15:10 +0100 |
wenzelm |
removed obsolete Proof General commands;
|
changeset |
files
|
| Fri, 31 Oct 2014 15:08:51 +0100 |
wenzelm |
obsolete;
|
changeset |
files
|
| Fri, 31 Oct 2014 11:36:41 +0100 |
wenzelm |
discontinued obsolete Output.urgent_message;
|
changeset |
files
|
| Fri, 31 Oct 2014 11:18:17 +0100 |
wenzelm |
discontinued Proof General;
|
changeset |
files
|
| Fri, 31 Oct 2014 17:01:54 +0000 |
paulson |
Some comments and a new version of a result
|
changeset |
files
|
| Thu, 30 Oct 2014 23:14:11 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 30 Oct 2014 22:45:19 +0100 |
wenzelm |
eliminated aliases;
|
changeset |
files
|
| Thu, 30 Oct 2014 16:55:29 +0100 |
wenzelm |
eliminated aliases;
|
changeset |
files
|
| Thu, 30 Oct 2014 16:20:46 +0100 |
wenzelm |
eliminated aliases;
|
changeset |
files
|
| Thu, 30 Oct 2014 16:17:56 +0100 |
wenzelm |
tuned spelling;
|
changeset |
files
|
| Thu, 30 Oct 2014 15:57:13 +0100 |
wenzelm |
hardwired imitation of copy.shortcut2 default;
|
changeset |
files
|
| Thu, 30 Oct 2014 21:02:01 +0100 |
haftmann |
more simp rules concerning dvd and even/odd
|
changeset |
files
|
| Thu, 30 Oct 2014 16:36:44 +0000 |
paulson |
choose_reduce_nat: re-ordered operands
|
changeset |
files
|
| Thu, 30 Oct 2014 11:24:53 +0100 |
wenzelm |
make SML/NJ more happy;
|
changeset |
files
|
| Thu, 30 Oct 2014 11:08:26 +0100 |
wenzelm |
proper syntax categery "name" -- as usual and as documented;
|
changeset |
files
|
| Thu, 30 Oct 2014 09:15:54 +0100 |
hoelzl |
disable coercions for NO_MATCH
|
changeset |
files
|
| Wed, 29 Oct 2014 19:26:05 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 29 Oct 2014 19:13:19 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 19:23:32 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 29 Oct 2014 19:01:49 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 17:01:44 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 15:28:27 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 15:15:17 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 15:07:53 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 15:02:29 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 14:40:14 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 14:14:36 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 14:05:36 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 13:57:20 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 13:42:38 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 11:41:54 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 11:33:29 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 11:19:27 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 29 Oct 2014 11:13:24 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 10:58:41 +0100 |
wenzelm |
modernized setup;
|
changeset |
files
|
| Wed, 29 Oct 2014 10:35:00 +0100 |
wenzelm |
more standard theory name;
|
changeset |
files
|
| Wed, 29 Oct 2014 09:42:46 +0100 |
wenzelm |
more iterators;
|
changeset |
files
|
| Wed, 29 Oct 2014 12:01:39 +0100 |
nipkow |
removed useless lemmas
|
changeset |
files
|
| Wed, 29 Oct 2014 11:03:23 +0100 |
nipkow |
tuned layout and proofs
|
changeset |
files
|
| Tue, 28 Oct 2014 17:16:22 +0100 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Tue, 28 Oct 2014 16:44:58 +0100 |
wenzelm |
increase chances that HOL-Proofs image still works for polyml-5.3.0;
|
changeset |
files
|
| Tue, 28 Oct 2014 16:27:11 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 28 Oct 2014 16:20:26 +0100 |
wenzelm |
proper selectMatch, e.g. relevant for S-click on gutter;
|
changeset |
files
|
| Tue, 28 Oct 2014 16:19:04 +0100 |
wenzelm |
find command span in buffer;
|
changeset |
files
|
| Tue, 28 Oct 2014 13:52:54 +0100 |
wenzelm |
'notepad' requires proper nesting of begin/end;
|
changeset |
files
|
| Tue, 28 Oct 2014 11:42:51 +0100 |
wenzelm |
explicit keyword category for commands that may start a block;
|
changeset |
files
|
| Tue, 28 Oct 2014 11:27:57 +0100 |
wenzelm |
updated keywords;
|
changeset |
files
|
| Tue, 28 Oct 2014 10:35:38 +0100 |
wenzelm |
'oops' requires proper goal statement -- exclude 'notepad' to avoid disrupting begin/end structure;
|
changeset |
files
|
| Tue, 28 Oct 2014 09:57:12 +0100 |
wenzelm |
more abstract type;
|
changeset |
files
|
| Tue, 28 Oct 2014 09:32:18 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 28 Oct 2014 09:20:07 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 27 Oct 2014 20:31:51 +0100 |
wenzelm |
updated to jdk-7u72;
|
changeset |
files
|
| Mon, 27 Oct 2014 20:21:56 +0100 |
wenzelm |
increase chances that HOL-Proofs image still works for polyml-5.3.0;
|
changeset |
files
|
| Mon, 27 Oct 2014 20:20:53 +0100 |
wenzelm |
JRE is sufficient for official release -- javac and jar are only needed for self-build;
|
changeset |
files
|
| Mon, 27 Oct 2014 16:11:24 +0100 |
wenzelm |
clarified ISABELLE_JDK_HOME vs. JAVA_HOME;
|
changeset |
files
|
| Mon, 27 Oct 2014 16:00:04 +0100 |
wenzelm |
ISABELLE_JAVA_EXT is obsolete;
|
changeset |
files
|
| Mon, 27 Oct 2014 12:21:24 +0100 |
hoelzl |
further generalization of natfloor_div_nat
|
changeset |
files
|
| Mon, 27 Oct 2014 12:03:13 +0100 |
hoelzl |
generalize natfloor_div_nat, add floor variant: floor_divide_real_eq_div
|
changeset |
files
|
| Sun, 26 Oct 2014 19:11:16 +0100 |
haftmann |
eliminated redundancies;
|
changeset |
files
|
| Sat, 25 Oct 2014 19:20:28 +0200 |
haftmann |
more simp rules;
|
changeset |
files
|
| Sun, 26 Oct 2014 15:57:10 +0100 |
wenzelm |
clarified default;
|
changeset |
files
|
| Sun, 26 Oct 2014 15:46:02 +0100 |
wenzelm |
support negative extraLineSpacing;
|
changeset |
files
|
| Sat, 25 Oct 2014 21:16:32 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Sat, 25 Oct 2014 11:53:35 +0200 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Fri, 24 Oct 2014 20:49:23 +0200 |
wenzelm |
merged;
|
changeset |
files
|
| Fri, 24 Oct 2014 11:30:39 +0200 |
wenzelm |
discontinued python from standard system environment;
|
changeset |
files
|
| Fri, 24 Oct 2014 11:05:19 +0200 |
wenzelm |
more generous default;
|
changeset |
files
|
| Thu, 23 Oct 2014 19:40:41 +0200 |
haftmann |
even further downshift of theory Parity in the hierarchy
|
changeset |
files
|
| Thu, 23 Oct 2014 19:40:39 +0200 |
haftmann |
further downshift of theory Parity in the hierarchy
|
changeset |
files
|
| Fri, 24 Oct 2014 15:07:51 +0200 |
hoelzl |
use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
|
changeset |
files
|
| Fri, 24 Oct 2014 15:07:49 +0200 |
hoelzl |
move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
|
changeset |
files
|
| Thu, 23 Oct 2014 16:25:08 +0200 |
haftmann |
repaired long-standing accident
|
changeset |
files
|
| Thu, 23 Oct 2014 14:43:51 +0200 |
haftmann |
explicit definition restores HOL Light import after cb9d84d3e7f2
|
changeset |
files
|
| Thu, 23 Oct 2014 14:43:48 +0200 |
haftmann |
tuned language and spelling
|
changeset |
files
|
| Thu, 23 Oct 2014 14:04:05 +0200 |
haftmann |
slight generalization and unification of simp rules for algebraic procedures
|
changeset |
files
|
| Thu, 23 Oct 2014 14:04:05 +0200 |
haftmann |
downshift of theory Parity in the hierarchy
|
changeset |
files
|
| Thu, 23 Oct 2014 14:04:05 +0200 |
haftmann |
parity induction over natural numbers
|
changeset |
files
|
| Wed, 22 Oct 2014 23:15:40 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 22 Oct 2014 17:34:01 +0200 |
wenzelm |
proper line height and text base line, like regular TextAreaPainter.PaintText;
|
changeset |
files
|
| Wed, 22 Oct 2014 17:30:58 +0200 |
wenzelm |
tuned imports;
|
changeset |
files
|
| Wed, 22 Oct 2014 17:34:19 +0200 |
Andreas Lochbihler |
merged
|
changeset |
files
|
| Wed, 22 Oct 2014 13:58:30 +0200 |
Andreas Lochbihler |
add print translation for probability notation \<P>
|
changeset |
files
|
| Wed, 22 Oct 2014 17:04:45 +0200 |
wenzelm |
find main command keyword of 'begin';
|
changeset |
files
|
| Wed, 22 Oct 2014 16:44:57 +0200 |
wenzelm |
restricted scanning;
|
changeset |
files
|
| Wed, 22 Oct 2014 11:24:48 +0200 |
wenzelm |
repaired rail diagram (cf. 8450b944e58a);
|
changeset |
files
|
| Tue, 21 Oct 2014 22:18:06 +0200 |
wenzelm |
foldPainter like Windows L&F;
|
changeset |
files
|
| Tue, 21 Oct 2014 21:55:45 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 21 Oct 2014 21:35:45 +0200 |
wenzelm |
NEWS;
|
changeset |
files
|
| Tue, 21 Oct 2014 21:32:12 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Tue, 21 Oct 2014 21:20:45 +0200 |
wenzelm |
ignore improper tokens to avoid ambiguity of Range.touches (assuming that relevant tokens are separated properly);
|
changeset |
files
|
| Tue, 21 Oct 2014 21:02:36 +0200 |
wenzelm |
support for proof structure matching;
|
changeset |
files
|
| Tue, 21 Oct 2014 20:45:05 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 21 Oct 2014 20:44:17 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 21 Oct 2014 20:19:14 +0200 |
wenzelm |
support for begin/end matching;
|
changeset |
files
|
| Tue, 21 Oct 2014 20:18:37 +0200 |
wenzelm |
proper token kind;
|
changeset |
files
|
| Tue, 21 Oct 2014 19:20:48 +0200 |
wenzelm |
added option jedit_structure_limit;
|
changeset |
files
|
| Tue, 21 Oct 2014 17:49:51 +0200 |
wenzelm |
some structure matching, based on line token iterators;
|
changeset |
files
|
| Tue, 21 Oct 2014 15:21:44 +0200 |
wenzelm |
support for structure matching;
|
changeset |
files
|
| Tue, 21 Oct 2014 13:56:42 +0200 |
wenzelm |
tuned rendering;
|
changeset |
files
|
| Tue, 21 Oct 2014 13:21:59 +0200 |
wenzelm |
back to alternative fold painter, despite f03a9c57760a -- gutter painter seems to have changed in the meantime;
|
changeset |
files
|
| Tue, 21 Oct 2014 11:13:16 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 21 Oct 2014 10:58:19 +0200 |
wenzelm |
update_cartouches;
|
changeset |
files
|
| Tue, 21 Oct 2014 10:53:24 +0200 |
wenzelm |
clarified tree root;
|
changeset |
files
|
| Tue, 21 Oct 2014 10:00:25 +0200 |
wenzelm |
tuned spacing;
|
changeset |
files
|
| Tue, 21 Oct 2014 09:50:22 +0200 |
wenzelm |
clarified verbatim line breaks, e.g. relevant for Implementation mldecls;
|
changeset |
files
|
| Tue, 21 Oct 2014 21:10:44 +0200 |
haftmann |
turn even into an abbreviation
|
changeset |
files
|
| Tue, 21 Oct 2014 17:23:16 +0200 |
desharna |
update documentation for 'size_o_map'
|
changeset |
files
|
| Tue, 21 Oct 2014 17:23:14 +0200 |
desharna |
rename 'size_o_map' to 'size_gen_o_map'
|
changeset |
files
|
| Tue, 21 Oct 2014 17:23:14 +0200 |
desharna |
document 'size_gen'
|
changeset |
files
|
| Tue, 21 Oct 2014 17:23:13 +0200 |
desharna |
generate 'size_gen' for datatypes
|
changeset |
files
|
| Tue, 21 Oct 2014 17:23:13 +0200 |
desharna |
document 'map_o_corec'
|
changeset |
files
|
| Tue, 21 Oct 2014 17:23:12 +0200 |
desharna |
generate 'map_o_corec' for (co)datatypes
|
changeset |
files
|
| Tue, 21 Oct 2014 17:23:12 +0200 |
desharna |
move documentation of 'rec_o_map'
|
changeset |
files
|
| Tue, 21 Oct 2014 17:23:11 +0200 |
desharna |
move theorem 'rec_o_map'
|
changeset |
files
|
| Tue, 21 Oct 2014 17:23:10 +0200 |
desharna |
warn for not fully mutually (co)recursive types
|
changeset |
files
|
| Tue, 21 Oct 2014 17:00:42 +0200 |
hoelzl |
add transfer rule for set_pmf
|
changeset |
files
|
| Mon, 20 Oct 2014 18:33:14 +0200 |
hoelzl |
add tendsto_const and tendsto_ident_at as simp and intro rules
|
changeset |
files
|
| Mon, 20 Oct 2014 23:17:28 +0200 |
wenzelm |
tuned spacing;
|
changeset |
files
|
| Mon, 20 Oct 2014 22:46:17 +0200 |
wenzelm |
avoid odd ligatures;
|
changeset |
files
|
| Mon, 20 Oct 2014 21:48:03 +0200 |
wenzelm |
more accurate approximation of AST;
|
changeset |
files
|
| Mon, 20 Oct 2014 21:44:33 +0200 |
wenzelm |
tuned exposition of {* ... *};
|
changeset |
files
|
| Mon, 20 Oct 2014 21:32:54 +0200 |
wenzelm |
more antiquotations;
|
changeset |
files
|
| Mon, 20 Oct 2014 20:43:02 +0200 |
wenzelm |
more antiquotations;
|
changeset |
files
|
| Mon, 20 Oct 2014 17:56:23 +0200 |
kuncar |
register transfer rules from BNF and FP_Sugar
|
changeset |
files
|
| Mon, 20 Oct 2014 17:56:21 +0200 |
kuncar |
refactored
|
changeset |
files
|
| Mon, 20 Oct 2014 17:41:04 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 20 Oct 2014 17:02:46 +0200 |
wenzelm |
back to formal comment (see 23a380cc45f4, 3094b0edd6b5);
|
changeset |
files
|
| Mon, 20 Oct 2014 17:00:13 +0200 |
wenzelm |
repared document;
|
changeset |
files
|
| Mon, 20 Oct 2014 16:53:50 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 20 Oct 2014 16:52:36 +0200 |
wenzelm |
official support for "tt" style variants, avoid fragile \verb in LaTeX;
|
changeset |
files
|
| Mon, 20 Oct 2014 14:11:14 +0200 |
wenzelm |
removed dead code;
|
changeset |
files
|
| Mon, 20 Oct 2014 10:19:50 +0200 |
wenzelm |
suppress special Poly/ML location inBasis (see $ML_SOURCES/mlsource/MLCompiler/STRUCT_VALS.ML);
|
changeset |
files
|
| Mon, 20 Oct 2014 16:12:23 +0100 |
paulson |
tweaked
|
changeset |
files
|
| Mon, 20 Oct 2014 12:26:44 +0200 |
haftmann |
avoid unsafe simp rules
|
changeset |
files
|
| Mon, 20 Oct 2014 07:57:33 +0200 |
haftmann |
more standard declaration for presburger
|
changeset |
files
|
| Mon, 20 Oct 2014 07:45:58 +0200 |
haftmann |
augmented and tuned facts on even/odd and division
|
changeset |
files
|
| Sun, 19 Oct 2014 18:05:26 +0200 |
haftmann |
prefer generic elimination rules for even/odd over specialized unfold rules for nat
|
changeset |
files
|
| Sun, 19 Oct 2014 12:47:34 +0200 |
wenzelm |
NEWS;
|
changeset |
files
|
| Sun, 19 Oct 2014 12:07:03 +0200 |
wenzelm |
omit pointless nodes for proof commands etc.;
|
changeset |
files
|
| Sun, 19 Oct 2014 11:20:03 +0200 |
wenzelm |
tuned signature and modules;
|
changeset |
files
|
| Sat, 18 Oct 2014 22:50:35 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 18 Oct 2014 22:49:59 +0200 |
wenzelm |
NEWS;
|
changeset |
files
|
| Sat, 18 Oct 2014 22:41:36 +0200 |
wenzelm |
more folds;
|
changeset |
files
|
| Sat, 18 Oct 2014 22:02:10 +0200 |
wenzelm |
always apply precedingFoldLevels, avoid unclear shortcuts;
|
changeset |
files
|
| Sat, 18 Oct 2014 21:26:01 +0200 |
wenzelm |
make double-sure that line context is present, e.g. relevant for last line after visible text;
|
changeset |
files
|
| Sat, 18 Oct 2014 20:56:16 +0200 |
wenzelm |
clarified Line_Structure wrt. command span;
|
changeset |
files
|
| Sat, 18 Oct 2014 11:19:34 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 18 Oct 2014 10:50:40 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 18 Oct 2014 10:32:19 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 16 Oct 2014 21:24:42 +0200 |
wenzelm |
more explicit Line_Nesting;
|
changeset |
files
|
| Thu, 16 Oct 2014 12:24:19 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Thu, 16 Oct 2014 12:09:57 +0200 |
wenzelm |
support line context with depth;
|
changeset |
files
|
| Thu, 16 Oct 2014 10:59:43 +0200 |
wenzelm |
proper type comparison (amending cd4439d8799c);
|
changeset |
files
|
| Thu, 16 Oct 2014 10:43:34 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 16 Oct 2014 19:26:28 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 16 Oct 2014 19:26:27 +0200 |
haftmann |
standard elimination rule for even
|
changeset |
files
|
| Thu, 16 Oct 2014 19:26:26 +0200 |
haftmann |
tuned facts on even and power
|
changeset |
files
|
| Thu, 16 Oct 2014 19:26:14 +0200 |
haftmann |
restructured
|
changeset |
files
|
| Thu, 16 Oct 2014 19:26:13 +0200 |
haftmann |
even more cleanup
|
changeset |
files
|
| Thu, 16 Oct 2014 11:56:46 +0200 |
blanchet |
made SML/NJ happier
|
changeset |
files
|
| Wed, 15 Oct 2014 17:18:08 +0200 |
blanchet |
made SML/NJ happier
|
changeset |
files
|
| Wed, 15 Oct 2014 17:15:11 +0200 |
blanchet |
tuned whitespace
|
changeset |
files
|
| Tue, 14 Oct 2014 19:39:29 +0200 |
wenzelm |
buffer_line_context via untyped access;
|
changeset |
files
|
| Tue, 14 Oct 2014 19:38:41 +0200 |
wenzelm |
access class hierarchy;
|
changeset |
files
|
| Tue, 14 Oct 2014 08:23:23 +0200 |
haftmann |
legacy cleanup
|
changeset |
files
|
| Tue, 14 Oct 2014 08:23:23 +0200 |
haftmann |
more algebraic deductions for facts on even/odd
|
changeset |
files
|
| Tue, 14 Oct 2014 08:23:23 +0200 |
haftmann |
more algebraic deductions for facts on even/odd
|
changeset |
files
|
| Tue, 14 Oct 2014 08:23:23 +0200 |
haftmann |
purely algebraic characterization of even and odd
|
changeset |
files
|
| Tue, 14 Oct 2014 16:19:42 +0200 |
desharna |
document 'sel_transfer'
|
changeset |
files
|
| Tue, 14 Oct 2014 16:17:36 +0200 |
desharna |
generate 'sel_transfer' for (co)datatypes
|
changeset |
files
|
| Tue, 14 Oct 2014 16:17:34 +0200 |
desharna |
add 'kind' to 'cr_sugar'
|
changeset |
files
|
| Tue, 14 Oct 2014 15:39:57 +0200 |
desharna |
add 'fp_bnf' to 'bnf_sugar'
|
changeset |
files
|
| Tue, 14 Oct 2014 15:39:56 +0200 |
desharna |
preserve the structure of 'set_intros' theorem in ML
|
changeset |
files
|
| Tue, 14 Oct 2014 15:39:54 +0200 |
desharna |
preserve the structure of 'map_sel' theorem in ML
|
changeset |
files
|
| Tue, 14 Oct 2014 15:11:35 +0200 |
desharna |
preserve the structure of 'set_sel' theorem in ML
|
changeset |
files
|
| Tue, 14 Oct 2014 13:51:38 +0200 |
steckerm |
Fixed bug in waldmeister skolemization
|
changeset |
files
|
| Tue, 14 Oct 2014 10:52:46 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 13 Oct 2014 22:43:29 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 13 Oct 2014 21:57:40 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 13 Oct 2014 21:46:41 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 13 Oct 2014 21:41:29 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 13 Oct 2014 20:51:48 +0200 |
wenzelm |
obsolete;
|
changeset |
files
|
| Mon, 13 Oct 2014 20:29:30 +0200 |
wenzelm |
module Interpretation is superseded by Plugin;
|
changeset |
files
|
| Mon, 13 Oct 2014 20:25:10 +0200 |
wenzelm |
module Interpretation is superseded by Plugin;
|
changeset |
files
|
| Mon, 13 Oct 2014 20:24:24 +0200 |
wenzelm |
module Interpretation is superseded by Plugin;
|
changeset |
files
|
| Mon, 13 Oct 2014 19:34:10 +0200 |
wenzelm |
clarified load order;
|
changeset |
files
|
| Mon, 13 Oct 2014 18:45:48 +0200 |
wenzelm |
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
|
changeset |
files
|
| Mon, 13 Oct 2014 17:04:25 +0200 |
wenzelm |
support for indirections (defined entries), e.g. relevant for quickcheck and its sub-plugins;
|
changeset |
files
|
| Mon, 13 Oct 2014 15:45:23 +0200 |
wenzelm |
support for named plugins for definitional packages;
|
changeset |
files
|
| Mon, 13 Oct 2014 18:55:05 +0200 |
immler |
relaxed class constraints for exp
|
changeset |
files
|
| Mon, 13 Oct 2014 16:07:11 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Sun, 12 Oct 2014 21:52:45 +0200 |
blanchet |
special treatment of extensionality in minimizer
|
changeset |
files
|
| Sun, 12 Oct 2014 21:52:45 +0200 |
blanchet |
improved handling of extensionality in Isar proofs generated from LEO-II and Satallax
|
changeset |
files
|
| Sun, 12 Oct 2014 21:52:44 +0200 |
blanchet |
made SML/NJ happier
|
changeset |
files
|
| Sun, 12 Oct 2014 19:53:13 +0200 |
haftmann |
leftover from 3ccafeb9a1d1
|
changeset |
files
|
| Sun, 12 Oct 2014 17:05:35 +0200 |
haftmann |
some more facts on divisibility
|
changeset |
files
|
| Sun, 12 Oct 2014 17:05:34 +0200 |
haftmann |
generalized and consolidated some theorems concerning divisibility
|
changeset |
files
|
| Sun, 12 Oct 2014 16:31:43 +0200 |
haftmann |
eliminiated clone
|
changeset |
files
|
| Sun, 12 Oct 2014 16:31:28 +0200 |
haftmann |
more facts about abstract divisibility
|
changeset |
files
|
| Fri, 10 Oct 2014 19:55:32 +0200 |
haftmann |
specialized specification: avoid trivial instances
|
changeset |
files
|
| Thu, 09 Oct 2014 22:43:48 +0200 |
haftmann |
more foundational definition for predicate even
|
changeset |
files
|
| Fri, 10 Oct 2014 18:23:59 +0200 |
nipkow |
New example Bubblesort
|
changeset |
files
|
| Thu, 09 Oct 2014 16:47:56 +0200 |
haftmann |
formally completeted set of experimental static evaluation functions
|
changeset |
files
|
| Thu, 09 Oct 2014 17:31:50 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 09 Oct 2014 13:57:40 +0200 |
wenzelm |
afford slightly bigger JVM stack (see also f7ba30a816b9);
|
changeset |
files
|
| Thu, 09 Oct 2014 13:56:27 +0200 |
wenzelm |
prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within read-only directory (due to its bundled Cygwin and /tmp inside of it);
|
changeset |
files
|
| Thu, 09 Oct 2014 11:15:03 +0200 |
wenzelm |
prefer Unix standard-conformant $TMPDIR over hard-wired /tmp;
|
changeset |
files
|
| Thu, 09 Oct 2014 11:00:15 +0200 |
wenzelm |
proper @{cite} with bibtex entry (unchecked comment);
|
changeset |
files
|
| Thu, 09 Oct 2014 11:00:40 +0200 |
hoelzl |
fix document generation in Code_Test
|
changeset |
files
|
| Wed, 08 Oct 2014 18:10:17 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 08 Oct 2014 17:37:20 +0200 |
wenzelm |
eliminated some exotic combinators;
|
changeset |
files
|
| Wed, 08 Oct 2014 17:09:07 +0200 |
wenzelm |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
changeset |
files
|
| Wed, 08 Oct 2014 14:34:30 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 08 Oct 2014 13:55:43 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 08 Oct 2014 11:50:25 +0200 |
wenzelm |
clarified messages depending on options;
|
changeset |
files
|
| Wed, 08 Oct 2014 11:09:17 +0200 |
wenzelm |
simplified "sos" method;
|
changeset |
files
|
| Wed, 08 Oct 2014 10:15:04 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 08 Oct 2014 10:03:46 +0200 |
wenzelm |
tuned spelling;
|
changeset |
files
|
| Wed, 08 Oct 2014 10:22:00 +0200 |
hoelzl |
add Linear Temporal Logic on Streams
|
changeset |
files
|
| Wed, 08 Oct 2014 09:09:12 +0200 |
Andreas Lochbihler |
move Code_Test to HOL/Library;
|
changeset |
files
|
| Wed, 08 Oct 2014 00:13:39 +0200 |
wenzelm |
proper bibliography;
|
changeset |
files
|
| Tue, 07 Oct 2014 23:52:34 +0200 |
wenzelm |
more antiquotations;
|
changeset |
files
|
| Tue, 07 Oct 2014 23:29:43 +0200 |
wenzelm |
more bibtex entries;
|
changeset |
files
|
| Tue, 07 Oct 2014 23:12:08 +0200 |
wenzelm |
more antiquotations;
|
changeset |
files
|
| Tue, 07 Oct 2014 22:54:49 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Tue, 07 Oct 2014 22:35:11 +0200 |
wenzelm |
more antiquotations;
|
changeset |
files
|
| Tue, 07 Oct 2014 21:44:41 +0200 |
wenzelm |
clarified whitespace;
|
changeset |
files
|
| Tue, 07 Oct 2014 21:29:59 +0200 |
wenzelm |
more cartouches;
|
changeset |
files
|
| Tue, 07 Oct 2014 21:28:24 +0200 |
wenzelm |
more cartouches;
|
changeset |
files
|
| Tue, 07 Oct 2014 21:11:18 +0200 |
wenzelm |
more cartouches;
|
changeset |
files
|
| Tue, 07 Oct 2014 21:01:31 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 07 Oct 2014 20:59:46 +0200 |
wenzelm |
more cartouches;
|
changeset |
files
|
| Tue, 07 Oct 2014 20:43:18 +0200 |
wenzelm |
more cartouches;
|
changeset |
files
|
| Tue, 07 Oct 2014 20:34:17 +0200 |
wenzelm |
more symbols;
|
changeset |
files
|
| Tue, 07 Oct 2014 20:27:31 +0200 |
wenzelm |
more cartouches;
|
changeset |
files
|
| Tue, 07 Oct 2014 14:53:51 +0200 |
wenzelm |
added update_cartouches tool;
|
changeset |
files
|
| Tue, 07 Oct 2014 11:44:25 +0200 |
wenzelm |
removed pointless regexp flags;
|
changeset |
files
|
| Tue, 07 Oct 2014 14:02:24 +0200 |
hoelzl |
fix document generation for HOL-Probability
|
changeset |
files
|
| Tue, 07 Oct 2014 10:48:29 +0200 |
hoelzl |
move Stream theory from Datatype_Examples to Library
|
changeset |
files
|
| Tue, 07 Oct 2014 10:34:24 +0200 |
hoelzl |
add Giry monad
|
changeset |
files
|
| Mon, 06 Oct 2014 21:21:46 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Mon, 06 Oct 2014 19:55:49 +0200 |
wenzelm |
improved spelling of formal INCOMPATIBILITY in historic versions (!) -- to avoid ad-hoc word completion multiply such lapses;
|
changeset |
files
|
| Mon, 06 Oct 2014 19:40:22 +0200 |
nipkow |
merged
|
changeset |
files
|
| Mon, 06 Oct 2014 19:37:42 +0200 |
nipkow |
tuned spaces
|
changeset |
files
|
| Mon, 06 Oct 2014 19:19:16 +0200 |
blanchet |
avoid creating needless skolemization steps for SPASS
|
changeset |
files
|
| Mon, 06 Oct 2014 19:19:16 +0200 |
blanchet |
get rid of 'individual' type in DFG proofs
|
changeset |
files
|
| Mon, 06 Oct 2014 19:19:16 +0200 |
blanchet |
slightly nicer names
|
changeset |
files
|
| Mon, 06 Oct 2014 19:19:16 +0200 |
blanchet |
strengthened 'moura' method
|
changeset |
files
|
| Mon, 06 Oct 2014 19:19:16 +0200 |
blanchet |
improved unskolemization of SPASS problems
|
changeset |
files
|
| Mon, 06 Oct 2014 18:17:44 +0200 |
wenzelm |
more total parser;
|
changeset |
files
|
| Mon, 06 Oct 2014 18:11:16 +0200 |
wenzelm |
more defensive error handling -- token marker must not crash;
|
changeset |
files
|
| Mon, 06 Oct 2014 17:27:27 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 06 Oct 2014 17:26:30 +0200 |
wenzelm |
documentation of @{cite} and cite_macro;
|
changeset |
files
|
| Mon, 06 Oct 2014 16:54:35 +0200 |
wenzelm |
completion for bibtex entries;
|
changeset |
files
|
| Mon, 06 Oct 2014 14:21:38 +0200 |
wenzelm |
more accurate item name, depending on kind;
|
changeset |
files
|
| Mon, 06 Oct 2014 11:44:16 +0200 |
wenzelm |
back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
|
changeset |
files
|
| Mon, 06 Oct 2014 10:24:51 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 06 Oct 2014 16:27:31 +0200 |
hoelzl |
add measure space for (coinductive) streams
|
changeset |
files
|
| Mon, 06 Oct 2014 16:27:07 +0200 |
hoelzl |
add type for probability mass functions, i.e. discrete probability distribution
|
changeset |
files
|
| Mon, 06 Oct 2014 13:42:48 +0200 |
desharna |
refactor 'map_sel_thms' and 'set_sel_thms'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:41:37 +0200 |
desharna |
rename 'xtor_rel_thms' to 'xtor_rels'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:40:56 +0200 |
desharna |
rename 'xtor_set_thmss' to 'xtor_setss'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:40:31 +0200 |
desharna |
rename 'xtor_map_thms' to 'xtor_maps'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:40:02 +0200 |
desharna |
rename one of the two 'rel_eq_thms' to 'rel_code_thms'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:39:12 +0200 |
desharna |
rename 'xtor_co_rec_transfer_thms' to 'xtor_co_rec_transfers'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:38:40 +0200 |
desharna |
rename 'dtor_set_induct_thms' to 'dtor_set_inducts'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:38:13 +0200 |
desharna |
rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:37:38 +0200 |
desharna |
rename 'xtor_co_rec_o_map_thms' to 'xtor_co_rec_o_maps'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:36:48 +0200 |
desharna |
add 'set_inducts' to 'fp_sugar'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:36:47 +0200 |
desharna |
add 'common_set_inducts' to 'fp_sugar'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:36:42 +0200 |
desharna |
add 'rel_co_inducts' to 'fp_sugar'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:35:29 +0200 |
desharna |
add 'common_rel_co_induct' to 'fp_sugar'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:35:15 +0200 |
desharna |
add 'co_rec_transfers' to 'fp_sugar'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:35:03 +0200 |
desharna |
add 'co_rec_disc_iffs' to 'fp_sugar'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:34:49 +0200 |
desharna |
add 'disc_transfers' to 'fp_sugar'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:34:39 +0200 |
desharna |
add 'case_transfers' to 'fp_sugar'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:34:24 +0200 |
desharna |
add 'ctr_transfers' to 'fp_sugar'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:34:12 +0200 |
desharna |
add 'set_cases' to 'fp_sugar'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:34:04 +0200 |
desharna |
add 'set_intros' to 'fp_sugar'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:33:45 +0200 |
desharna |
add 'set_sels' to 'fp_sugar'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:33:36 +0200 |
desharna |
add 'set_thms' to 'fp_sugar'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:33:24 +0200 |
desharna |
add 'rel_cases' to 'fp_sugar'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:33:15 +0200 |
desharna |
add 'rel_intros' to 'fp_sugar'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:33:04 +0200 |
desharna |
add 'rel_sels' to 'fp_sugar'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:32:53 +0200 |
desharna |
add 'map_sels' to 'fp_sugar'
|
changeset |
files
|
| Mon, 06 Oct 2014 13:32:41 +0200 |
desharna |
add 'map_disc_iffs' to 'fp_sugar'
|
changeset |
files
|
| Sun, 05 Oct 2014 20:30:58 +0200 |
haftmann |
code preprocessor tracing also for function transformers
|
changeset |
files
|
| Sun, 05 Oct 2014 20:30:57 +0200 |
haftmann |
basic support for fully static evaluator generation without dynamic compiler invocation
|
changeset |
files
|
| Sun, 05 Oct 2014 20:30:56 +0200 |
haftmann |
split dynamic from static context
|
changeset |
files
|
| Sun, 05 Oct 2014 23:09:27 +0200 |
wenzelm |
more refs;
|
changeset |
files
|
| Sun, 05 Oct 2014 22:47:07 +0200 |
wenzelm |
prefer @{cite} antiquotation;
|
changeset |
files
|
| Sun, 05 Oct 2014 22:46:20 +0200 |
wenzelm |
prefer @{cite} antiquotation;
|
changeset |
files
|
| Sun, 05 Oct 2014 22:46:13 +0200 |
wenzelm |
prefer @{cite} antiquotation;
|
changeset |
files
|
| Sun, 05 Oct 2014 22:24:07 +0200 |
wenzelm |
prefer @{cite} antiquotation;
|
changeset |
files
|
| Sun, 05 Oct 2014 22:22:40 +0200 |
wenzelm |
NEWS;
|
changeset |
files
|
| Sun, 05 Oct 2014 22:18:40 +0200 |
wenzelm |
more explicit syntax, to avoid misunderstanding of foo-bar as 3 separate arguments;
|
changeset |
files
|
| Sun, 05 Oct 2014 18:44:04 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Sun, 05 Oct 2014 18:30:43 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Sun, 05 Oct 2014 18:21:39 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Sun, 05 Oct 2014 18:14:26 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Sun, 05 Oct 2014 17:58:36 +0200 |
wenzelm |
citation tooltip/hyperlink based on open buffers with .bib files;
|
changeset |
files
|
| Sun, 05 Oct 2014 16:05:17 +0200 |
wenzelm |
bibtex support in ML: document antiquotation @{cite} with markup;
|
changeset |
files
|
| Sun, 05 Oct 2014 15:05:26 +0200 |
wenzelm |
maintain Document_Model.bibtex_entries;
|
changeset |
files
|
| Sun, 05 Oct 2014 13:16:24 +0200 |
wenzelm |
more advanced NEWS tree structure and folding;
|
changeset |
files
|
| Sat, 04 Oct 2014 22:15:31 +0200 |
wenzelm |
merged;
|
changeset |
files
|
| Sat, 04 Oct 2014 22:15:22 +0200 |
wenzelm |
NEWS;
|
changeset |
files
|
| Sat, 04 Oct 2014 22:11:08 +0200 |
wenzelm |
tuned output;
|
changeset |
files
|
| Sat, 04 Oct 2014 19:26:31 +0200 |
wenzelm |
proper treatment of @comment (amending 402a8e8107a7);
|
changeset |
files
|
| Sat, 04 Oct 2014 18:26:25 +0200 |
wenzelm |
mark hard tabs as single chunks, as required by jEdit (see 0fd2bf8eaa9f);
|
changeset |
files
|
| Sat, 04 Oct 2014 18:16:24 +0200 |
wenzelm |
more total chunk_line: recovery via ignored_line;
|
changeset |
files
|
| Sat, 04 Oct 2014 18:05:30 +0200 |
wenzelm |
more explicit comments;
|
changeset |
files
|
| Sat, 04 Oct 2014 17:57:03 +0200 |
wenzelm |
clarified nesting of delimiters;
|
changeset |
files
|
| Sat, 04 Oct 2014 16:11:39 +0200 |
wenzelm |
fields are case-insensitive;
|
changeset |
files
|
| Sat, 04 Oct 2014 16:02:17 +0200 |
wenzelm |
clarified nesting of delimiters;
|
changeset |
files
|
| Sat, 04 Oct 2014 15:34:25 +0200 |
wenzelm |
more explicit chunk name;
|
changeset |
files
|
| Sat, 04 Oct 2014 15:11:29 +0200 |
wenzelm |
clarified Chunk -- avoid ooddities;
|
changeset |
files
|
| Sat, 04 Oct 2014 12:19:26 +0200 |
wenzelm |
support for bibtex token markup;
|
changeset |
files
|
| Fri, 03 Oct 2014 23:33:47 +0200 |
wenzelm |
more explicit item kind;
|
changeset |
files
|
| Fri, 03 Oct 2014 20:19:42 +0200 |
wenzelm |
strict spaces for item_start: despite actual bibtex syntax, but in accordance to bibtex modes in Emacs and jEdit;
|
changeset |
files
|
| Fri, 03 Oct 2014 14:46:26 +0200 |
wenzelm |
SideKick parser for bibtex entries;
|
changeset |
files
|
| Fri, 03 Oct 2014 11:16:28 +0200 |
wenzelm |
more buffer.isEditable checks;
|
changeset |
files
|
| Fri, 03 Oct 2014 11:03:37 +0200 |
wenzelm |
context menu for bibtex entries;
|
changeset |
files
|
| Thu, 02 Oct 2014 11:54:30 +0200 |
wenzelm |
some support for bibtex files;
|
changeset |
files
|
| Fri, 03 Oct 2014 11:55:07 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Fri, 03 Oct 2014 11:48:27 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Thu, 02 Oct 2014 17:51:04 +0200 |
haftmann |
accomplish potentially case-insenstive file systems for Scala
|
changeset |
files
|
| Thu, 02 Oct 2014 22:33:45 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Thu, 02 Oct 2014 20:04:00 +0200 |
blanchet |
merge
|
changeset |
files
|
| Thu, 02 Oct 2014 18:10:09 +0200 |
blanchet |
more precise lemma insertion
|
changeset |
files
|
| Thu, 02 Oct 2014 17:40:46 +0200 |
blanchet |
insert lemmas closer to where they are needed, both for esthetics and (primarily) for correctness in case the lemma refers to a skolem
|
changeset |
files
|
| Thu, 02 Oct 2014 17:39:38 +0200 |
blanchet |
avoid duplicate 'obtain' in veriT Isar proofs, by removing dubious condition
|
changeset |
files
|
| Thu, 02 Oct 2014 15:24:51 +0200 |
blanchet |
eliminate duplicate hypotheses (which can arise due to (un)clausification)
|
changeset |
files
|
| Thu, 02 Oct 2014 11:33:08 +0200 |
haftmann |
formal lcm definition for polynomials
|
changeset |
files
|
| Thu, 02 Oct 2014 11:33:06 +0200 |
haftmann |
moved lemmas out of Int.thy which have nothing to do with int
|
changeset |
files
|
| Thu, 02 Oct 2014 11:33:05 +0200 |
haftmann |
redundant: dropped
|
changeset |
files
|
| Thu, 02 Oct 2014 11:33:04 +0200 |
haftmann |
tuned Heap_Monad.successE
|
changeset |
files
|
| Thu, 02 Oct 2014 12:02:29 +0200 |
blanchet |
documentation
|
changeset |
files
|
| Thu, 02 Oct 2014 12:02:28 +0200 |
blanchet |
fixed a few mistakes in the documentation
|
changeset |
files
|
| Thu, 02 Oct 2014 12:02:27 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 02 Oct 2014 11:01:20 +0200 |
blanchet |
'moura' method is also useful for reconstructing skolemization of lambda-lifting of formulas for other provers than Z3
|
changeset |
files
|
| Wed, 01 Oct 2014 21:00:49 +0200 |
wenzelm |
actually finish after closing, e.g. relevant for consecutive (**)(**);
|
changeset |
files
|
| Tue, 30 Sep 2014 22:43:20 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Tue, 30 Sep 2014 19:37:34 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 30 Sep 2014 18:44:01 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Tue, 30 Sep 2014 16:40:03 +0200 |
blanchet |
don't call 'hd' on a possibly empty list
|
changeset |
files
|
| Tue, 30 Sep 2014 16:01:46 +0200 |
blanchet |
proper types for applied variables, for typed formats (TFF0, DFG)
|
changeset |
files
|
| Tue, 30 Sep 2014 15:18:01 +0200 |
blanchet |
don't affect other subgoals with 'auto' in one-liner proofs
|
changeset |
files
|
| Tue, 30 Sep 2014 14:54:14 +0200 |
blanchet |
tuned output in case of one-liner failure
|
changeset |
files
|
| Tue, 30 Sep 2014 14:40:48 +0200 |
blanchet |
updated docs with two provers: veriT and Zipperposition
|
changeset |
files
|
| Tue, 30 Sep 2014 14:19:25 +0200 |
blanchet |
give more facts to veriT -- it seems to be able to cope with them
|
changeset |
files
|
| Tue, 30 Sep 2014 14:18:07 +0200 |
blanchet |
use native encoding with Vampire -- modern versions handle types better than the old ones
|
changeset |
files
|
| Tue, 30 Sep 2014 14:18:07 +0200 |
blanchet |
always minimize, to reinvoke the prover with nicer options and yield a nicer Isar proof (potentially -- cf. 'full_proof')
|
changeset |
files
|
| Tue, 30 Sep 2014 14:01:33 +0200 |
fleury |
correct inlining in veriT's subproofs.
|
changeset |
files
|
| Tue, 30 Sep 2014 12:47:15 +0200 |
blanchet |
repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'
|
changeset |
files
|
| Tue, 30 Sep 2014 11:34:20 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 30 Sep 2014 11:19:30 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 30 Sep 2014 11:06:26 +0200 |
blanchet |
keep rules with no premises in Isar proofs from veriT
|
changeset |
files
|
| Tue, 30 Sep 2014 10:25:04 +0200 |
blanchet |
correct indexing in the presence of lambda-lifting
|
changeset |
files
|
| Mon, 29 Sep 2014 22:09:17 +0200 |
nipkow |
merged
|
changeset |
files
|
| Mon, 29 Sep 2014 22:09:05 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Mon, 29 Sep 2014 21:40:02 +0200 |
blanchet |
merge
|
changeset |
files
|
| Mon, 29 Sep 2014 20:26:04 +0200 |
blanchet |
support hypotheses with schematics in Isar proofs
|
changeset |
files
|
| Mon, 29 Sep 2014 21:34:48 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Mon, 29 Sep 2014 18:37:33 +0200 |
blanchet |
simplified and repaired veriT index handling code
|
changeset |
files
|
| Mon, 29 Sep 2014 14:32:30 +0200 |
blanchet |
made 'moura' tactic more powerful
|
changeset |
files
|
| Mon, 29 Sep 2014 12:30:12 +0200 |
blanchet |
fixed wrong optimization (wrong because it may affect the sequent's conclusion)
|
changeset |
files
|
| Mon, 29 Sep 2014 12:30:09 +0200 |
blanchet |
merge
|
changeset |
files
|
| Mon, 29 Sep 2014 12:29:52 +0200 |
blanchet |
added option to get cleaner SPASS proofs
|
changeset |
files
|
| Mon, 29 Sep 2014 10:39:39 +0200 |
blanchet |
parse back type of SPASS proof variables
|
changeset |
files
|
| Mon, 29 Sep 2014 10:39:39 +0200 |
blanchet |
make sure no '__' suffixes make it until Isar proof
|
changeset |
files
|
| Mon, 29 Sep 2014 10:39:39 +0200 |
blanchet |
rename skolem symbols in the negative case as well
|
changeset |
files
|
| Mon, 29 Sep 2014 10:39:39 +0200 |
blanchet |
reintroduced 'rel_cases' in docs
|
changeset |
files
|
| Mon, 29 Sep 2014 10:39:39 +0200 |
blanchet |
added options to Mirabelle
|
changeset |
files
|
| Mon, 29 Sep 2014 10:39:39 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 29 Sep 2014 11:18:25 +0200 |
wenzelm |
faster machine for slow/bulky polyml-5.3.0 tests (notably HOL-Proofs);
|
changeset |
files
|
| Mon, 29 Sep 2014 09:57:34 +0200 |
wenzelm |
pro-forma support for polyml-5.5.3 (presently SVN 1960);
|
changeset |
files
|
| Mon, 29 Sep 2014 08:13:23 +0200 |
haftmann |
corrected white-space accident
|
changeset |
files
|
| Sun, 28 Sep 2014 20:27:47 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Sun, 28 Sep 2014 20:27:46 +0200 |
haftmann |
moved to HOL and generalized
|
changeset |
files
|
| Fri, 26 Sep 2014 19:38:26 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 26 Sep 2014 15:10:02 +0200 |
wenzelm |
proper range for Antiq tokens;
|
changeset |
files
|
| Fri, 26 Sep 2014 15:05:11 +0200 |
wenzelm |
support for sub-expression markup;
|
changeset |
files
|
| Fri, 26 Sep 2014 14:29:06 +0200 |
wenzelm |
tuned message;
|
changeset |
files
|
| Fri, 26 Sep 2014 14:43:28 +0200 |
desharna |
refactor fp_sugar move theorems
|
changeset |
files
|
| Fri, 26 Sep 2014 14:43:26 +0200 |
desharna |
refactor fp_sugar move theorems
|
changeset |
files
|
| Fri, 26 Sep 2014 14:41:54 +0200 |
desharna |
refactor fp_sugar move theorems
|
changeset |
files
|
| Fri, 26 Sep 2014 14:41:15 +0200 |
desharna |
refactor fp_sugar move theorems
|
changeset |
files
|
| Fri, 26 Sep 2014 14:41:08 +0200 |
desharna |
refactor fp_sugar move theorems
|
changeset |
files
|
| Fri, 26 Sep 2014 14:36:54 +0200 |
desharna |
refactor fp_sugar with empty substructures
|
changeset |
files
|
| Fri, 26 Sep 2014 14:35:09 +0200 |
desharna |
add attribute 'case_names' to 'set_case'
|
changeset |
files
|
| Fri, 26 Sep 2014 09:58:35 +0200 |
desharna |
make 'case_transfer' tactic more robust
|
changeset |
files
|
| Thu, 25 Sep 2014 18:47:32 +0200 |
haftmann |
more correct precedence of do-notation
|
changeset |
files
|
| Thu, 25 Sep 2014 17:07:44 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 25 Sep 2014 15:01:42 +0200 |
wenzelm |
save image as PNG or PDF;
|
changeset |
files
|
| Thu, 25 Sep 2014 12:22:12 +0200 |
wenzelm |
support for PNG output;
|
changeset |
files
|
| Thu, 25 Sep 2014 10:36:39 +0200 |
wenzelm |
more isatests (on lxbroy4);
|
changeset |
files
|
| Thu, 25 Sep 2014 16:35:56 +0200 |
desharna |
document 'corec_transfer'
|
changeset |
files
|
| Thu, 25 Sep 2014 16:35:56 +0200 |
desharna |
generate 'corec_transfer' for codatatypes
|
changeset |
files
|
| Thu, 25 Sep 2014 16:35:54 +0200 |
desharna |
document 'rec_transfer'
|
changeset |
files
|
| Thu, 25 Sep 2014 16:35:53 +0200 |
desharna |
generate 'rec_transfer' for datatypes
|
changeset |
files
|
| Thu, 25 Sep 2014 16:35:51 +0200 |
desharna |
generate 'dtor_corec_transfer' for codatatypes
|
changeset |
files
|
| Thu, 25 Sep 2014 16:35:50 +0200 |
desharna |
generate 'ctor_rec_transfer' for datatypes
|
changeset |
files
|
| Mon, 01 Sep 2014 14:14:47 +0200 |
traytel |
goal generation for xtor_co_rec_transfer
|
changeset |
files
|
| Thu, 25 Sep 2014 13:30:57 +0200 |
blanchet |
commented out some tests that require external tools (e.g. ghc)
|
changeset |
files
|
| Thu, 25 Sep 2014 13:30:57 +0200 |
blanchet |
added useful options to CVC4
|
changeset |
files
|
| Thu, 25 Sep 2014 12:27:34 +0200 |
traytel |
subscribe for isatest
|
changeset |
files
|
| Thu, 25 Sep 2014 09:01:14 +0200 |
traytel |
even more deads go to the end (continuation of e3a01b73579f)
|
changeset |
files
|
| Thu, 25 Sep 2014 11:38:56 +0200 |
nipkow |
added function size1
|
changeset |
files
|
| Wed, 24 Sep 2014 19:11:21 +0200 |
haftmann |
added lemmas
|
changeset |
files
|
| Wed, 24 Sep 2014 19:10:30 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Wed, 24 Sep 2014 21:00:07 +0200 |
blanchet |
avoid type variable name clash
|
changeset |
files
|
| Wed, 24 Sep 2014 21:00:07 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 24 Sep 2014 17:33:53 +0200 |
blanchet |
made N2M tests conditional, since they appear to cause Isatest timeouts and are kind of slow
|
changeset |
files
|
| Wed, 24 Sep 2014 16:35:42 +0200 |
blanchet |
improved 'bnf' parser
|
changeset |
files
|
| Wed, 24 Sep 2014 15:46:41 +0200 |
blanchet |
updated SMT certificates
|
changeset |
files
|
| Wed, 24 Sep 2014 15:46:40 +0200 |
blanchet |
allow homogeneous nesting for SMT (co)datatypes
|
changeset |
files
|
| Wed, 24 Sep 2014 15:46:25 +0200 |
blanchet |
interleave (co)datatypes in the right order w.r.t. dependencies
|
changeset |
files
|
| Wed, 24 Sep 2014 15:46:24 +0200 |
blanchet |
rule out nested (co)recursion for SMT (co)datatypes
|
changeset |
files
|
| Wed, 24 Sep 2014 15:46:23 +0200 |
blanchet |
gracefully handle types like 'enat' whose coinductive view is registered using 'free_constructors'
|
changeset |
files
|
| Wed, 24 Sep 2014 15:46:11 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 24 Sep 2014 15:45:55 +0200 |
blanchet |
simpler proof
|
changeset |
files
|
| Wed, 24 Sep 2014 11:09:05 +0200 |
nipkow |
added nice standard syntax
|
changeset |
files
|
| Mon, 22 Sep 2014 21:45:59 +0200 |
wenzelm |
clarified timeout for isatest;
|
changeset |
files
|
| Mon, 22 Sep 2014 21:31:45 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 22 Sep 2014 21:28:57 +0200 |
wenzelm |
discontinued old "xnum" token category;
|
changeset |
files
|
| Mon, 22 Sep 2014 17:07:18 +0200 |
wenzelm |
added csdp-6.x for proof method (sos csdp);
|
changeset |
files
|
| Mon, 22 Sep 2014 16:28:24 +0200 |
wenzelm |
examples for local CSDP executable;
|
changeset |
files
|
| Mon, 22 Sep 2014 16:15:29 +0200 |
wenzelm |
clarified SOS tool setup vs. examples;
|
changeset |
files
|
| Mon, 22 Sep 2014 15:01:27 +0200 |
desharna |
make 'set_induct0' tactic more robust w.r.t multiple arguments constructors
|
changeset |
files
|
| Mon, 22 Sep 2014 10:55:51 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 22 Sep 2014 10:18:41 +0200 |
wenzelm |
clarified ISABELLE_POLYML;
|
changeset |
files
|
| Mon, 22 Sep 2014 10:53:54 +0200 |
Andreas Lochbihler |
drop workaround addressed by d0d3c30806b4
|
changeset |
files
|
| Sun, 21 Sep 2014 20:22:12 +0200 |
wenzelm |
renamed ISABELLE_POLYML to ML_SYSTEM_POLYML, to avoid overlap with ISABELLE_POLYML_PATH;
|
changeset |
files
|
| Sun, 21 Sep 2014 20:14:04 +0200 |
wenzelm |
more standard Isabelle/ML operations;
|
changeset |
files
|
| Sun, 21 Sep 2014 19:53:50 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 21 Sep 2014 16:56:11 +0200 |
haftmann |
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
|
changeset |
files
|
| Sun, 21 Sep 2014 16:56:06 +0200 |
haftmann |
corrected slip in documentation
|
changeset |
files
|
| Sat, 20 Sep 2014 10:44:24 +0200 |
steckerm |
Removed double space
|
changeset |
files
|
| Sat, 20 Sep 2014 10:44:24 +0200 |
steckerm |
Changed proof method to auto for custom Waldmeister lemma
|
changeset |
files
|
| Sat, 20 Sep 2014 10:44:24 +0200 |
steckerm |
Minor fixes in ATP_Waldmeister
|
changeset |
files
|
| Sat, 20 Sep 2014 10:44:23 +0200 |
steckerm |
Made encoded type for apply less restrictive
|
changeset |
files
|
| Sat, 20 Sep 2014 10:44:23 +0200 |
steckerm |
Updated fix_name function
|
changeset |
files
|
| Sat, 20 Sep 2014 10:42:08 +0200 |
steckerm |
Added support for partial function application
|
changeset |
files
|
| Sat, 20 Sep 2014 10:42:08 +0200 |
steckerm |
Improved equality handling in skolemization
|
changeset |
files
|
| Sat, 20 Sep 2014 10:42:08 +0200 |
steckerm |
Re-added hypothesis argument to problem generation
|
changeset |
files
|
| Thu, 18 Sep 2014 18:48:54 +0200 |
haftmann |
always annotate potentially polymorphic Haskell numerals
|
changeset |
files
|
| Thu, 18 Sep 2014 18:48:04 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 18 Sep 2014 18:48:04 +0200 |
haftmann |
simplified and tuned using signed_string_of_int
|
changeset |
files
|
| Thu, 18 Sep 2014 18:48:04 +0200 |
haftmann |
tuned data structure
|
changeset |
files
|
| Fri, 19 Sep 2014 14:24:03 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 19 Sep 2014 14:08:21 +0200 |
blanchet |
documented limitations
|
changeset |
files
|
| Fri, 19 Sep 2014 13:41:40 +0200 |
blanchet |
more honest 'primcorec' -- don't parse a theorem name that is then ignored
|
changeset |
files
|
| Fri, 19 Sep 2014 13:38:21 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 19 Sep 2014 13:27:04 +0200 |
blanchet |
added a few tests for 'old_datatype'
|
changeset |
files
|
| Fri, 19 Sep 2014 13:27:04 +0200 |
blanchet |
reintroduced old setup for size of basic types
|
changeset |
files
|
| Fri, 19 Sep 2014 13:27:04 +0200 |
blanchet |
keep obsolete interpretations in Main, to avoid merge trouble
|
changeset |
files
|
| Fri, 19 Sep 2014 13:27:04 +0200 |
blanchet |
made new 'primrec' bootstrapping-capable
|
changeset |
files
|
| Fri, 19 Sep 2014 13:27:04 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 19 Sep 2014 13:27:04 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 19 Sep 2014 10:40:56 +0200 |
traytel |
typo
|
changeset |
files
|
| Fri, 19 Sep 2014 10:00:34 +0200 |
traytel |
regression tests for n2m
|
changeset |
files
|
| Fri, 19 Sep 2014 08:26:03 +0200 |
Andreas Lochbihler |
merged
|
changeset |
files
|
| Thu, 18 Sep 2014 15:23:23 +0200 |
Andreas Lochbihler |
add lemma
|
changeset |
files
|
| Thu, 18 Sep 2014 19:01:50 +0200 |
blanchet |
tuned imports
|
changeset |
files
|
| Thu, 18 Sep 2014 18:49:58 +0200 |
blanchet |
removed debugging junk
|
changeset |
files
|
| Thu, 18 Sep 2014 17:54:56 +0200 |
blanchet |
help AFP entry 'Free-Groups' to compile
|
changeset |
files
|
| Thu, 18 Sep 2014 16:57:10 +0200 |
blanchet |
reintroduced an instantiation of 'size' for 'numerals'
|
changeset |
files
|
| Thu, 18 Sep 2014 16:47:40 +0200 |
blanchet |
use selector
|
changeset |
files
|
| Thu, 18 Sep 2014 16:47:40 +0200 |
blanchet |
moved old 'size' generator together with 'old_datatype'
|
changeset |
files
|
| Thu, 18 Sep 2014 16:47:40 +0200 |
blanchet |
moved datatype realizer to 'old_datatype' and colleagues
|
changeset |
files
|
| Thu, 18 Sep 2014 16:47:40 +0200 |
blanchet |
careful with op = in n2m (actually by Dmitriy Traytel)
|
changeset |
files
|
| Thu, 18 Sep 2014 16:47:40 +0200 |
blanchet |
fixed attribute name in docs (thanks to Andreas Lochbihler)
|
changeset |
files
|
| Thu, 18 Sep 2014 16:47:40 +0200 |
blanchet |
updated NEWS
|
changeset |
files
|
| Thu, 18 Sep 2014 16:47:40 +0200 |
blanchet |
moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
|
changeset |
files
|
| Thu, 18 Sep 2014 16:47:40 +0200 |
blanchet |
increased 'HOL-Proofs' timeout
|
changeset |
files
|
| Thu, 18 Sep 2014 16:47:40 +0200 |
blanchet |
made 'mk_pointfree' work again in local theories
|
changeset |
files
|
| Thu, 18 Sep 2014 16:47:40 +0200 |
blanchet |
fixed authorship
|
changeset |
files
|
| Thu, 18 Sep 2014 15:07:43 +0200 |
haftmann |
product over monoids for lists
|
changeset |
files
|
| Thu, 18 Sep 2014 00:03:46 +0200 |
blanchet |
renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
|
changeset |
files
|
| Thu, 18 Sep 2014 00:02:45 +0200 |
blanchet |
more meaningful record tests
|
changeset |
files
|
| Thu, 18 Sep 2014 00:01:27 +0200 |
blanchet |
updated SMT certificates
|
changeset |
files
|
| Wed, 17 Sep 2014 23:45:57 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 17 Sep 2014 23:45:28 +0200 |
blanchet |
take out selectors for records -- for derived records, these don't quite have the right type
|
changeset |
files
|
| Wed, 17 Sep 2014 21:35:58 +0200 |
blanchet |
register Isabelle selectors as SMT selectors when possible
|
changeset |
files
|
| Wed, 17 Sep 2014 17:32:27 +0200 |
blanchet |
added codatatype support for CVC4
|
changeset |
files
|
| Wed, 17 Sep 2014 16:53:39 +0200 |
blanchet |
added interface for CVC4 extensions
|
changeset |
files
|
| Wed, 17 Sep 2014 16:20:13 +0200 |
blanchet |
avoid 'subst_tac' when possible (it is suspected of not helping 'HOL-Proofs')
|
changeset |
files
|
| Wed, 17 Sep 2014 12:09:33 +0200 |
blanchet |
tweaked compatibility layer
|
changeset |
files
|
| Wed, 17 Sep 2014 11:54:59 +0200 |
blanchet |
avoid clash with Quickcheck's generated 'random_xxx' function
|
changeset |
files
|
| Wed, 17 Sep 2014 11:12:46 +0200 |
blanchet |
added missing 'restore' in 'transfer' plugin
|
changeset |
files
|
| Wed, 17 Sep 2014 08:24:10 +0200 |
blanchet |
syntactic check to determine when to prove 'nested_size_o_map'
|
changeset |
files
|
| Wed, 17 Sep 2014 08:23:53 +0200 |
blanchet |
support (finite values of) codatatypes in Quickcheck
|
changeset |
files
|
| Tue, 16 Sep 2014 19:23:37 +0200 |
blanchet |
tuned fact visibility
|
changeset |
files
|
| Tue, 16 Sep 2014 19:23:37 +0200 |
blanchet |
register 'prod' and 'sum' as datatypes, to allow N2M through them
|
changeset |
files
|
| Tue, 16 Sep 2014 19:23:37 +0200 |
blanchet |
took out 'old_datatype' examples -- those just cause timeouts in Isatests
|
changeset |
files
|
| Tue, 16 Sep 2014 19:23:37 +0200 |
blanchet |
added 'extraction' plugins -- this might help 'HOL-Proofs'
|
changeset |
files
|
| Tue, 16 Sep 2014 18:42:33 +0200 |
nipkow |
added lemma
|
changeset |
files
|
| Tue, 16 Sep 2014 16:04:08 +0200 |
Andreas Lochbihler |
add target language evaluators for the value command;
|
changeset |
files
|
| Mon, 15 Sep 2014 18:12:09 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 15 Sep 2014 17:56:37 +0200 |
blanchet |
refactoring
|
changeset |
files
|
| Mon, 15 Sep 2014 16:34:05 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 15 Sep 2014 16:14:14 +0200 |
blanchet |
set 'mono' attribute on 'rel_mono'
|
changeset |
files
|
| Mon, 15 Sep 2014 16:11:01 +0200 |
blanchet |
'code' is needed for extraction datatype
|
changeset |
files
|
| Mon, 15 Sep 2014 14:31:32 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 15 Sep 2014 12:30:06 +0200 |
blanchet |
removed accidental '@{print}'
|
changeset |
files
|
| Mon, 15 Sep 2014 12:11:41 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 15 Sep 2014 11:54:47 +0200 |
blanchet |
more hints on how to port 'size'
|
changeset |
files
|
| Mon, 15 Sep 2014 11:37:55 +0200 |
blanchet |
tuned definition of 'size' function to get nicer properties
|
changeset |
files
|
| Mon, 15 Sep 2014 11:17:44 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 15 Sep 2014 11:10:09 +0200 |
blanchet |
document size difference
|
changeset |
files
|
| Mon, 15 Sep 2014 10:49:07 +0200 |
blanchet |
generate 'code' attribute only if 'code' plugin is enabled
|
changeset |
files
|
| Sun, 14 Sep 2014 22:59:30 +0200 |
blanchet |
disable datatype 'plugins' for internal types
|
changeset |
files
|
| Sat, 13 Sep 2014 18:08:45 +0200 |
blanchet |
ported Imperative HOL to new datatypes
|
changeset |
files
|
| Sat, 13 Sep 2014 18:08:38 +0200 |
blanchet |
imported patch phantoms
|
changeset |
files
|
| Fri, 12 Sep 2014 17:51:31 +0200 |
blanchet |
enabled 'Sudoku' only with 'ISABELLE_FULL_TEST' -- Sudoku is fast enough on modern hardware (within seconds on my MacBook), but it seems to fail on older test machines
|
changeset |
files
|
| Fri, 12 Sep 2014 17:30:05 +0200 |
blanchet |
new datatype is too slow on the huge datatypes (at least the mutual ones) -- use 'old_datatype' instead
|
changeset |
files
|
| Fri, 12 Sep 2014 16:42:36 +0200 |
blanchet |
run larger nominal examples only 'ISABELLE_FULL_TEST'
|
changeset |
files
|
| Fri, 12 Sep 2014 13:50:55 +0200 |
desharna |
refactor repeated terms in a single variable
|
changeset |
files
|
| Fri, 12 Sep 2014 13:50:51 +0200 |
desharna |
make 'ctr_transfer' tactic more robust
|
changeset |
files
|
| Fri, 12 Sep 2014 13:48:15 +0200 |
desharna |
make 'rel_sel' and 'map_sel' tactics more robust
|
changeset |
files
|
| Fri, 12 Sep 2014 13:27:33 +0200 |
fleury |
Changing the way the dependencies are managed.
|
changeset |
files
|
| Fri, 12 Sep 2014 13:27:32 +0200 |
fleury |
correction in the thf0 parser ("(=)" found in a Satallax proof).
|
changeset |
files
|
| Fri, 12 Sep 2014 11:17:06 +0200 |
blanchet |
merge
|
changeset |
files
|
| Fri, 12 Sep 2014 11:16:47 +0200 |
blanchet |
fixed spellings
|
changeset |
files
|
| Fri, 12 Sep 2014 07:38:15 +0200 |
haftmann |
NEWS
|
changeset |
files
|
| Thu, 11 Sep 2014 23:12:32 +0200 |
haftmann |
abstract product over monoid for lists
|
changeset |
files
|
| Thu, 11 Sep 2014 18:33:56 +0200 |
haftmann |
use proto_base_sort uniformly
|
changeset |
files
|
| Thu, 11 Sep 2014 21:11:03 +0200 |
blanchet |
fixed some spelling mistakes
|
changeset |
files
|
| Thu, 11 Sep 2014 20:01:29 +0200 |
blanchet |
tuned comment
|
changeset |
files
|
| Thu, 11 Sep 2014 19:59:46 +0200 |
blanchet |
more porting to new datatypes
|
changeset |
files
|
| Thu, 11 Sep 2014 19:45:42 +0200 |
blanchet |
tuning terminology
|
changeset |
files
|
| Thu, 11 Sep 2014 19:41:45 +0200 |
blanchet |
compile
|
changeset |
files
|
| Thu, 11 Sep 2014 19:39:48 +0200 |
blanchet |
renamed example theory for consistency
|
changeset |
files
|
| Thu, 11 Sep 2014 19:38:22 +0200 |
blanchet |
updated ROOT
|
changeset |
files
|
| Thu, 11 Sep 2014 19:35:38 +0200 |
blanchet |
tuned documentation
|
changeset |
files
|
| Thu, 11 Sep 2014 19:32:36 +0200 |
blanchet |
updated news
|
changeset |
files
|
| Thu, 11 Sep 2014 19:26:59 +0200 |
blanchet |
renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
|
changeset |
files
|
| Thu, 11 Sep 2014 19:20:23 +0200 |
blanchet |
move datatype benchmarks
|
changeset |
files
|
| Thu, 11 Sep 2014 19:18:23 +0200 |
blanchet |
use new datatypes for benchmarks
|
changeset |
files
|
| Thu, 11 Sep 2014 18:54:36 +0200 |
blanchet |
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
|
changeset |
files
|
| Thu, 11 Sep 2014 18:54:36 +0200 |
blanchet |
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
|
changeset |
files
|
| Thu, 11 Sep 2014 18:54:36 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 11 Sep 2014 18:54:36 +0200 |
blanchet |
fixed situation in 'primrec' when recursive calls are apparently nested, e.g. 'f (f x y) y', with the recursion in 'y'
|
changeset |
files
|
| Thu, 11 Sep 2014 18:54:36 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 11 Sep 2014 18:54:36 +0200 |
blanchet |
fixed situation in 'primrec' whereby the original value of a constructor argument of nested type was not translated correctly to a 'map fst'
|
changeset |
files
|
| Thu, 11 Sep 2014 18:54:36 +0200 |
blanchet |
speed up old Nominal by killing type variables
|
changeset |
files
|
| Thu, 11 Sep 2014 18:54:36 +0200 |
blanchet |
took out some datatype tests for Refute -- these yield timeouts on some Isatests after transition to new datatypes, for some reason (and Refute is obsolete anyway)
|
changeset |
files
|
| Thu, 11 Sep 2014 18:54:36 +0200 |
blanchet |
more docs
|
changeset |
files
|
| Thu, 11 Sep 2014 15:08:56 +0200 |
traytel |
new deads go to the end
|
changeset |
files
|
| Thu, 11 Sep 2014 11:49:47 +0200 |
blanchet |
comment
|
changeset |
files
|
| Wed, 10 Sep 2014 22:52:46 +0200 |
haftmann |
more material on lists
|
changeset |
files
|
| Wed, 10 Sep 2014 14:58:02 +0200 |
haftmann |
explicit check phase to guide type inference of class expression towards one single type variable
|
changeset |
files
|
| Wed, 10 Sep 2014 14:58:01 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Wed, 10 Sep 2014 14:57:03 +0200 |
haftmann |
dropped ineffective print_translation which has never been adjusted to check/uncheck-style case patterns
|
changeset |
files
|
| Tue, 09 Sep 2014 23:54:47 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 09 Sep 2014 23:54:39 +0200 |
blanchet |
proper checks -- the calls data structure may contain spurious entries
|
changeset |
files
|
| Tue, 09 Sep 2014 22:33:43 +0200 |
blanchet |
avoid exception
|
changeset |
files
|
| Tue, 09 Sep 2014 22:28:49 +0200 |
blanchet |
avoid internal fact
|
changeset |
files
|
| Tue, 09 Sep 2014 22:25:14 +0200 |
blanchet |
restored old case names
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
compile
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
avoid duplicate case names
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
nicer case names in the N2M case, similar to those generated by the old package (e.g. 'Cons_tree' instead of just 'Cons')
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
preserve case names in '(co)induct' theorems generated by prim(co)rec'
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
hide DEADID/ID theorems
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
more canonical (and correct) local theory threading
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
removed 'datatype_compat's that are no longer needed
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
documented extraction plugin
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
made realizer more robust in the face of nesting through functions
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
removed debugging junk
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
renamed ML file and module
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
made datatype realizer plugin work for new-style datatypes with no nesting
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
ported HOL-Proofs-Lambda to new datatypes
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
ported HOL-Proofs-Extraction to new datatypes
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
made SML/NJ happier
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
more porting to new datatypes
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
tuned IArray code generator w.r.t. map rel set
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
ported Nitpick_Examples to new datatypes
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
set 'fundef_cong' attribute also for (co)datatypes with no live type variables
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
ported IArray to new datatypes
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
prevent infinite loop when type variables are of a non-'type' sort
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
tuned code
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
ported MicroJava to new datatypes
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
rename_tac'd scrips
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
ported Unix to new datatypes
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
ported Isar_Examples to new datatypes
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
ported Decision_Procs to new datatypes
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
ported Induct to new datatypes
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
half-ported Imperative HOL to new datatypes
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
tuned messages
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
rename_tac'd scripts
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
reverted 83a8570b44bc, which was a misunderstanding
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
rename_tac'd script
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
ported Bali to new datatypes
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
rename_tac'd scripts
|
changeset |
files
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
|
changeset |
files
|
| Tue, 09 Sep 2014 17:51:07 +0200 |
nipkow |
merged
|
changeset |
files
|
| Tue, 09 Sep 2014 17:50:54 +0200 |
nipkow |
enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
|
changeset |
files
|
| Tue, 09 Sep 2014 15:33:01 +0200 |
steckerm |
Fixed bug which broke isar proof construction for all ATPs except Waldmeister_new
|
changeset |
files
|
| Mon, 08 Sep 2014 23:09:37 +0200 |
blanchet |
more docs
|
changeset |
files
|
| Mon, 08 Sep 2014 23:09:34 +0200 |
blanchet |
more documentation
|
changeset |
files
|
| Mon, 08 Sep 2014 23:09:25 +0200 |
blanchet |
made 'lifting' plugin more robust
|
changeset |
files
|
| Mon, 08 Sep 2014 23:09:24 +0200 |
blanchet |
tuned command descriptions
|
changeset |
files
|
| Mon, 08 Sep 2014 23:09:23 +0200 |
blanchet |
generate better internal names, with name of the target type in it
|
changeset |
files
|
| Mon, 08 Sep 2014 23:09:04 +0200 |
blanchet |
removed comment (yes, this is different -- add_typedef_global will fail in a locale with assumptions)
|
changeset |
files
|
| Mon, 08 Sep 2014 23:04:18 +0200 |
blanchet |
added flag to 'typedef' to allow concealed definitions
|
changeset |
files
|
| Mon, 08 Sep 2014 23:04:18 +0200 |
blanchet |
ported old Nominal to use new datatypes
|
changeset |
files
|
| Mon, 08 Sep 2014 20:42:52 +0200 |
traytel |
made tactic even more robust w.r.t. dead variables
|
changeset |
files
|
| Mon, 08 Sep 2014 19:21:19 +0200 |
blanchet |
made N2M work with sort constraints (cf. TODO)
|
changeset |
files
|
| Mon, 08 Sep 2014 19:21:14 +0200 |
blanchet |
compile
|
changeset |
files
|
| Mon, 08 Sep 2014 19:21:07 +0200 |
blanchet |
honour sorts in N2M
|
changeset |
files
|
| Mon, 08 Sep 2014 16:51:35 +0200 |
blanchet |
proper sort constraints in map and rel theorems
|
changeset |
files
|
| Mon, 08 Sep 2014 16:22:26 +0200 |
blanchet |
made new countable tactic work with sorts other than 'type'
|
changeset |
files
|
| Mon, 08 Sep 2014 16:14:21 +0200 |
blanchet |
adapted examples to latest changes
|
changeset |
files
|
| Mon, 08 Sep 2014 16:09:10 +0200 |
blanchet |
made code work also in the presence of deads
|
changeset |
files
|
| Mon, 08 Sep 2014 15:54:33 +0200 |
blanchet |
export right sorts
|
changeset |
files
|
| Mon, 08 Sep 2014 15:12:35 +0200 |
blanchet |
test sorts
|
changeset |
files
|
| Mon, 08 Sep 2014 15:11:37 +0200 |
blanchet |
use right sort constraints
|
changeset |
files
|
| Mon, 08 Sep 2014 14:04:03 +0200 |
blanchet |
never include hidden names -- these cannot be referenced afterward
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:57 +0200 |
blanchet |
use compatibility layer
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:46 +0200 |
blanchet |
made SML/NJ happire
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:40 +0200 |
blanchet |
export useful functions for users of (co)recursors
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:35 +0200 |
blanchet |
improved caching
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:13 +0200 |
blanchet |
compile
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:08 +0200 |
blanchet |
wildcards in plugins
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:02 +0200 |
blanchet |
improved 'datatype_compat' further for recursion through functions
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:02 +0200 |
blanchet |
no type-based lookup -- these fail in the general, ambiguous case
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:02 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:02 +0200 |
blanchet |
more examples/tests
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:02 +0200 |
blanchet |
tuned docs
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
properly note theorems for split recursors
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
updated docs
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
export one more ML function
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
more compatibility documentation
|
changeset |
files
|
| Mon, 08 Sep 2014 13:56:28 +0200 |
blanchet |
refactored MaSh files to avoid regenerating exports on each eval
|
changeset |
files
|
| Mon, 08 Sep 2014 13:56:27 +0200 |
blanchet |
added missing 'transpose'
|
changeset |
files
|
| Mon, 08 Sep 2014 13:56:27 +0200 |
blanchet |
the kind is now always the empty string -- can no longer distinguish between user theorems and package theorems in a semi-reliable way
|
changeset |
files
|
| Mon, 08 Sep 2014 09:52:06 +0200 |
traytel |
made tactic more robust w.r.t. dead variables
|
changeset |
files
|
| Sun, 07 Sep 2014 17:51:32 +0200 |
haftmann |
restrictive options for class dependencies
|
changeset |
files
|
| Sun, 07 Sep 2014 17:51:28 +0200 |
haftmann |
separated class_deps command into separate file
|
changeset |
files
|
| Sun, 07 Sep 2014 14:39:23 +0200 |
steckerm |
Added translation for lambda expressions in terms.
|
changeset |
files
|
| Sun, 07 Sep 2014 09:49:05 +0200 |
haftmann |
explicit theory with additional, less commonly used list operations
|
changeset |
files
|
| Sun, 07 Sep 2014 09:49:01 +0200 |
haftmann |
generalized
|
changeset |
files
|
| Sat, 06 Sep 2014 20:12:36 +0200 |
haftmann |
theory about sum and product on function bodies
|
changeset |
files
|
| Sat, 06 Sep 2014 20:12:34 +0200 |
haftmann |
theory about lexicographic ordering on functions
|
changeset |
files
|
| Sat, 06 Sep 2014 20:12:32 +0200 |
haftmann |
added various facts
|
changeset |
files
|
| Fri, 05 Sep 2014 16:09:03 +0100 |
paulson |
Generalised card_length_listsum to all m
|
changeset |
files
|
| Fri, 05 Sep 2014 14:58:13 +0200 |
nipkow |
added lemma
|
changeset |
files
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
updated docs
|
changeset |
files
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
pretend code generation is a ctr_sugar plugin
|
changeset |
files
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
updated docs
|
changeset |
files
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
added 'plugins' option to control which hooks are enabled
|
changeset |
files
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
introduced mechanism to filter interpretations
|
changeset |
files
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
fixed infinite loops in 'register' functions + more uniform API
|
changeset |
files
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
named interpretations
|
changeset |
files
|
| Fri, 05 Sep 2014 00:41:00 +0200 |
blanchet |
centralized and cleaned up naming handling
|
changeset |
files
|
| Thu, 04 Sep 2014 14:02:37 +0200 |
hoelzl |
cleanup Wfrec; introduce dependent_wf/wellorder_choice
|
changeset |
files
|
| Thu, 04 Sep 2014 11:53:39 +0200 |
blanchet |
tuned Nitpick and Refute examples, which are too slow on some testing machines
|
changeset |
files
|
| Thu, 04 Sep 2014 11:20:59 +0200 |
blanchet |
tweaked setup for datatype realizer
|
changeset |
files
|
| Thu, 04 Sep 2014 09:02:43 +0200 |
blanchet |
renamed internal constant
|
changeset |
files
|
| Thu, 04 Sep 2014 09:02:43 +0200 |
blanchet |
moved code around
|
changeset |
files
|
| Thu, 04 Sep 2014 09:02:43 +0200 |
blanchet |
tuned size function generation
|
changeset |
files
|
| Thu, 04 Sep 2014 09:02:36 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 03 Sep 2014 22:49:05 +0200 |
blanchet |
introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:48 +0200 |
blanchet |
tuned ctr_sugar database handling
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:35 +0200 |
blanchet |
tuned BNF database handling
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:09 +0200 |
blanchet |
intelligible errors instead of tactic failures
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
reenabled yet another example
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
made new tactic even more robust
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
reenabled more examples
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
fixed tactic for n-way mutual recursion, n >= 4 (balanced conjunctions confuse the tactic)
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
reintroduced more examples
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
improved tactic further
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
reenabled example
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
improved new countability tactic
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
more robust exception handling
|
changeset |
files
|
| Wed, 03 Sep 2014 22:46:54 +0200 |
blanchet |
added tests for new 'countable_datatype' proof method
|
changeset |
files
|
| Wed, 03 Sep 2014 12:30:25 +0200 |
traytel |
lessen the burden on the caller: sort where necessary in n2m
|
changeset |
files
|
| Wed, 03 Sep 2014 09:43:00 +0200 |
blanchet |
added compatibility function
|
changeset |
files
|
| Wed, 03 Sep 2014 00:31:38 +0200 |
blanchet |
added countable tactic for new-style datatypes
|
changeset |
files
|
| Wed, 03 Sep 2014 00:31:37 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:32 +0200 |
blanchet |
registered 'typerep' as countable again
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:30 +0200 |
blanchet |
moved old datatype material around
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:28 +0200 |
blanchet |
removed vacuous theorem references
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:27 +0200 |
blanchet |
commented out failing tactic (now that 'typerep' is defined using the new package
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:26 +0200 |
blanchet |
tuned imports
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:25 +0200 |
blanchet |
use 'datatype_new'
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:24 +0200 |
blanchet |
use 'datatype_new' in 'Main'
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:23 +0200 |
blanchet |
take out 'x = C' of the simplifier for unit types
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:22 +0200 |
blanchet |
giving up calling 'datatype_compat' in a locale -- causes trouble with extensions
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:22 +0200 |
blanchet |
ported 'Statespace' to support new datatypes as well
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:21 +0200 |
blanchet |
use 'datatype_new' in Quickcheck examples
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:19 +0200 |
blanchet |
more compatibility functions
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:18 +0200 |
blanchet |
codatatypes are not datatypes
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:17 +0200 |
blanchet |
ported Quickcheck to support new datatypes better
|
changeset |
files
|
| Tue, 02 Sep 2014 23:59:49 +0200 |
blanchet |
removed more slow Refute tests
|
changeset |
files
|
| Tue, 02 Sep 2014 23:59:46 +0200 |
blanchet |
tuned Refute example
|
changeset |
files
|
| Tue, 02 Sep 2014 16:38:26 +0200 |
steckerm |
Some work on the new waldmeister integration
|
changeset |
files
|
| Tue, 02 Sep 2014 14:40:32 +0200 |
boehmes |
merged
|
changeset |
files
|
| Tue, 02 Sep 2014 14:40:14 +0200 |
boehmes |
replay Z3 rewrite steps that lift if-then-else expressions
|
changeset |
files
|
| Tue, 02 Sep 2014 13:40:03 +0200 |
traytel |
test discriminators/selectors in BNF regression suite
|
changeset |
files
|
| Tue, 02 Sep 2014 12:13:32 +0200 |
blanchet |
merge
|
changeset |
files
|
| Tue, 02 Sep 2014 12:11:04 +0200 |
blanchet |
made SML/NJ happier
|
changeset |
files
|
| Tue, 02 Sep 2014 12:09:13 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 02 Sep 2014 09:28:23 +0200 |
traytel |
silenced nonexhaustive primrec warnings
|
changeset |
files
|
| Tue, 02 Sep 2014 08:24:42 +0200 |
haftmann |
more convenient printing of real numbers after evaluation
|
changeset |
files
|
| Mon, 01 Sep 2014 19:58:25 +0200 |
blanchet |
avoid more 'bad background theory' issues
|
changeset |
files
|
| Mon, 01 Sep 2014 19:57:48 +0200 |
blanchet |
ported TFL to mixture of old and new datatypes
|
changeset |
files
|
| Mon, 01 Sep 2014 19:28:00 +0200 |
blanchet |
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
|
changeset |
files
|
| Mon, 01 Sep 2014 18:42:02 +0200 |
blanchet |
ported to use new-style datatypes
|
changeset |
files
|
| Mon, 01 Sep 2014 17:34:03 +0200 |
blanchet |
ported Refute to use new datatypes when possible
|
changeset |
files
|
| Mon, 01 Sep 2014 16:34:40 +0200 |
blanchet |
renamed BNF theories
|
changeset |
files
|
| Mon, 01 Sep 2014 16:34:39 +0200 |
blanchet |
renamed '(BNF_)Constructions_on_Wellorders' to '(BNF_)Wellorder_Constructions'
|
changeset |
files
|
| Mon, 01 Sep 2014 16:34:38 +0200 |
blanchet |
added primrec compatibility function
|
changeset |
files
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
more work on compatibility interfaces
|
changeset |
files
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
added compatibility examples/tests
|
changeset |
files
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
implemented compatibility definition of datatype
|
changeset |
files
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
implemented compatibility interpretation
|
changeset |
files
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
compile
|
changeset |
files
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
compile
|
changeset |
files
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
compile
|
changeset |
files
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
more compatibility between old- and new-style datatypes
|
changeset |
files
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
added theory-based getters for convenience
|
changeset |
files
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
made transfer functions slightly more general
|
changeset |
files
|
| Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
tuned signatures
|
changeset |
files
|
| Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
|
changeset |
files
|
| Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
tuned structure inclusion
|
changeset |
files
|
| Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
took out legacy material from 'HOL/Library/Library.thy'
|
changeset |
files
|
| Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
removed commented out parts
|
changeset |
files
|
| Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
tuned whitespace
|
changeset |
files
|
| Mon, 01 Sep 2014 13:53:39 +0200 |
desharna |
document 'set_transfer'
|
changeset |
files
|
| Mon, 01 Sep 2014 13:53:34 +0200 |
desharna |
generate 'set_transfer' for BNFs
|
changeset |
files
|
| Mon, 01 Sep 2014 13:23:41 +0200 |
desharna |
document 'rel_transfer'
|
changeset |
files
|
| Mon, 01 Sep 2014 13:23:39 +0200 |
desharna |
generate 'rel_transfer' for BNFs
|
changeset |
files
|
| Mon, 01 Sep 2014 13:23:05 +0200 |
desharna |
document 'map_transfer'
|
changeset |
files
|
| Mon, 01 Sep 2014 13:23:00 +0200 |
desharna |
note 'map_transfer' more often
|
changeset |
files
|
| Sun, 31 Aug 2014 09:10:42 +0200 |
haftmann |
separated listsum material
|
changeset |
files
|
| Sun, 31 Aug 2014 09:10:41 +0200 |
haftmann |
restored generic value slot, retaining default behaviour and separate approximate command
|
changeset |
files
|
| Sun, 31 Aug 2014 09:10:40 +0200 |
haftmann |
convenient printing of (- 1 :: integer) after code evaluation
|
changeset |
files
|
| Sat, 30 Aug 2014 11:15:47 +0200 |
haftmann |
inlined unused definition
|
changeset |
files
|
| Fri, 29 Aug 2014 11:24:31 +0200 |
hoelzl |
add simp rules for divisions of numerals in floor and ceiling.
|
changeset |
files
|
| Fri, 29 Aug 2014 14:48:23 +0200 |
desharna |
document 'disc_transfer'
|
changeset |
files
|
| Fri, 29 Aug 2014 14:36:51 +0200 |
desharna |
generate 'disc_transfer' for (co)datatypes
|
changeset |
files
|
| Fri, 29 Aug 2014 14:21:25 +0200 |
desharna |
document 'case_transfer'
|
changeset |
files
|
| Fri, 29 Aug 2014 14:21:24 +0200 |
desharna |
generate 'case_transfer' for (co)datatypes
|
changeset |
files
|
| Thu, 28 Aug 2014 23:57:26 +0200 |
blanchet |
renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
|
changeset |
files
|
| Thu, 28 Aug 2014 23:48:46 +0200 |
blanchet |
reworked unskolemization for SPASS
|
changeset |
files
|
| Thu, 28 Aug 2014 20:06:59 +0200 |
blanchet |
clarified docs
|
changeset |
files
|
| Thu, 28 Aug 2014 20:05:39 +0200 |
blanchet |
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
|
changeset |
files
|
| Thu, 28 Aug 2014 19:07:10 +0200 |
blanchet |
prefer '0.2 ms' to '249 \<mu>s'
|
changeset |
files
|
| Thu, 28 Aug 2014 19:02:37 +0200 |
blanchet |
use 'thesis' only if it expands to the right thing (it won't after an 'unfolding', for example)
|
changeset |
files
|
| Thu, 28 Aug 2014 17:25:56 +0200 |
blanchet |
fixed second computations
|
changeset |
files
|
| Thu, 28 Aug 2014 16:58:27 +0200 |
blanchet |
merged minimize and auto_minimize
|
changeset |
files
|
| Thu, 28 Aug 2014 16:58:27 +0200 |
blanchet |
pass options to remote Vampire
|
changeset |
files
|
| Thu, 28 Aug 2014 16:58:27 +0200 |
blanchet |
removed show stuttering
|
changeset |
files
|
| Thu, 28 Aug 2014 16:58:27 +0200 |
blanchet |
generate 'thesis' variable in Sledgehammer Isar proofs
|
changeset |
files
|
| Thu, 28 Aug 2014 16:58:27 +0200 |
blanchet |
show microseconds as well (useful when playing with Isar proofs)
|
changeset |
files
|
| Thu, 28 Aug 2014 16:58:27 +0200 |
blanchet |
tuned message
|
changeset |
files
|
| Thu, 28 Aug 2014 16:58:27 +0200 |
blanchet |
made trace more informative when minimization is enabled
|
changeset |
files
|
| Thu, 28 Aug 2014 16:58:27 +0200 |
blanchet |
took out one more occurrence of 'PolyML.makestring'
|
changeset |
files
|
| Thu, 28 Aug 2014 16:58:27 +0200 |
blanchet |
try 'skolem' method first for Z3
|
changeset |
files
|
| Thu, 28 Aug 2014 16:58:27 +0200 |
blanchet |
tuned tracing output (indirectly)
|
changeset |
files
|
| Thu, 28 Aug 2014 16:58:27 +0200 |
blanchet |
going back to bc06471cb7b7 for silencing -- the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
|
changeset |
files
|
| Thu, 28 Aug 2014 16:58:27 +0200 |
blanchet |
moved skolem method
|
changeset |
files
|
| Thu, 28 Aug 2014 16:58:27 +0200 |
blanchet |
added 'skolem' method, esp. for 'obtain's generated from Z3 proofs
|
changeset |
files
|
| Thu, 28 Aug 2014 16:58:26 +0200 |
blanchet |
tuned method description
|
changeset |
files
|
| Thu, 28 Aug 2014 16:58:26 +0200 |
blanchet |
three-line 'obtain' format for generated Isar proofs
|
changeset |
files
|
| Thu, 28 Aug 2014 15:51:50 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 28 Aug 2014 15:47:26 +0200 |
wenzelm |
more liberal embedded "text", which includes cartouches;
|
changeset |
files
|
| Thu, 28 Aug 2014 13:25:12 +0200 |
wenzelm |
intern xthm only once;
|
changeset |
files
|
| Thu, 28 Aug 2014 07:34:23 +0200 |
blanchet |
tuned terminology
|
changeset |
files
|
| Thu, 28 Aug 2014 07:30:16 +0200 |
blanchet |
moved new para to right section of NEWS
|
changeset |
files
|
| Thu, 28 Aug 2014 00:40:38 +0200 |
blanchet |
minor NEWS fix
|
changeset |
files
|
| Thu, 28 Aug 2014 00:40:38 +0200 |
blanchet |
keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
|
changeset |
files
|
| Thu, 28 Aug 2014 00:40:38 +0200 |
blanchet |
added 'OLD_' prefix in front of old solvers
|
changeset |
files
|
| Thu, 28 Aug 2014 00:40:38 +0200 |
blanchet |
updated NEWS
|
changeset |
files
|
| Thu, 28 Aug 2014 00:40:38 +0200 |
blanchet |
renamed new SMT module from 'SMT2' to 'SMT'
|
changeset |
files
|
| Thu, 28 Aug 2014 00:40:38 +0200 |
blanchet |
updated NEWS
|
changeset |
files
|
| Thu, 28 Aug 2014 00:40:38 +0200 |
blanchet |
prefixed all old SMT commands, attributes, etc., with 'old_'
|
changeset |
files
|
| Thu, 28 Aug 2014 00:40:38 +0200 |
blanchet |
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
|
changeset |
files
|
| Thu, 28 Aug 2014 00:40:38 +0200 |
blanchet |
renaming theory 'Old_SMT'
|
changeset |
files
|
| Thu, 28 Aug 2014 00:40:37 +0200 |
blanchet |
moved old setup for SMT out
|
changeset |
files
|
| Thu, 28 Aug 2014 00:40:37 +0200 |
blanchet |
moved old 'smt' method out of 'Main'
|
changeset |
files
|
| Thu, 28 Aug 2014 00:40:37 +0200 |
blanchet |
reintroduced two-line-per-inference Isar proof format
|
changeset |
files
|
| Thu, 28 Aug 2014 00:40:19 +0200 |
blanchet |
removed needless, and for (newer versions of?) Haskell problematic code equations
|
changeset |
files
|
| Wed, 27 Aug 2014 15:55:01 +0200 |
wenzelm |
removed obsolete RC tags;
|
changeset |
files
|
| Wed, 27 Aug 2014 15:52:58 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 27 Aug 2014 11:33:00 +0200 |
wenzelm |
Added tag Isabelle2014 for changeset 8f4a332500e4
|
changeset |
files
|
| Wed, 27 Aug 2014 14:55:33 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 27 Aug 2014 14:54:32 +0200 |
wenzelm |
more explicit Method.modifier with reported position;
|
changeset |
files
|
| Wed, 27 Aug 2014 12:32:42 +0200 |
wenzelm |
tuned signature -- prefer quasi-abstract Symbol_Pos.source;
|
changeset |
files
|
| Wed, 27 Aug 2014 12:32:07 +0200 |
wenzelm |
added ML antiquotation @{source} for Symbol_Pos.source;
|
changeset |
files
|
| Mon, 25 Aug 2014 12:58:20 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 27 Aug 2014 13:05:59 +0200 |
blanchet |
removed not so interesting 'set_empty'
|
changeset |
files
|
| Wed, 27 Aug 2014 08:41:12 +0200 |
blanchet |
avoid 'PolyML.makestring'
|
changeset |
files
|
| Mon, 25 Aug 2014 14:24:05 +0200 |
hoelzl |
introduce real_of typeclass for real :: 'a => real
|
changeset |
files
|
| Mon, 25 Aug 2014 16:06:41 +0200 |
nipkow |
added lemmas
|
changeset |
files
|
| Tue, 19 Aug 2014 18:37:32 +0200 |
hoelzl |
better linarith support for floor, ceiling, natfloor, and natceiling
|
changeset |
files
|
| Mon, 25 Aug 2014 09:40:50 +0200 |
Andreas Lochbihler |
add testing framework for generated code
|
changeset |
files
|
| Mon, 25 Aug 2014 09:08:45 +0200 |
Andreas Lochbihler |
correct code equation for term_of on integer
|
changeset |
files
|
| Mon, 25 Aug 2014 08:45:32 +0200 |
Andreas Lochbihler |
merged
|
changeset |
files
|
| Fri, 22 Aug 2014 14:39:40 +0200 |
Andreas Lochbihler |
add code equation for term_of on integer
|
changeset |
files
|
| Fri, 22 Aug 2014 17:35:48 +0200 |
blanchet |
added lemmas contributed by Rene Thiemann
|
changeset |
files
|
| Fri, 22 Aug 2014 15:55:24 +0200 |
wenzelm |
attach modifier only later, to avoid interference as e.g. in "simp add: foo [simplified] bar";
|
changeset |
files
|
| Fri, 22 Aug 2014 15:39:30 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Fri, 22 Aug 2014 12:05:47 +0200 |
wenzelm |
clarified ML toplevel pp: avoid ML output to be attached to inlined binding positions;
|
changeset |
files
|
| Fri, 22 Aug 2014 11:31:19 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 22 Aug 2014 11:28:51 +0200 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Thu, 21 Aug 2014 23:54:27 +0200 |
wenzelm |
clarified Method.section: explicit declaration with static closure;
|
changeset |
files
|
| Thu, 21 Aug 2014 22:48:39 +0200 |
wenzelm |
tuned signature -- define some elementary operations earlier;
|
changeset |
files
|
| Thu, 21 Aug 2014 13:46:29 +0200 |
wenzelm |
discontinued odd "temporary" workaround from 2006 (6ac7a4fc32a0), which has no measurable relevance;
|
changeset |
files
|
| Thu, 21 Aug 2014 13:31:31 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 21 Aug 2014 10:07:06 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 21 Aug 2014 09:48:59 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 22 Aug 2014 08:43:14 +0200 |
haftmann |
generic euclidean algorithm (due to Manuel Eberl)
|
changeset |
files
|
| Thu, 21 Aug 2014 14:41:08 +0200 |
haftmann |
integrated appendix theory into main theory;
|
changeset |
files
|
| Thu, 21 Aug 2014 14:41:05 +0200 |
haftmann |
dropped dead file
|
changeset |
files
|
| Thu, 21 Aug 2014 13:59:45 +0200 |
desharna |
fix tactic failure with rel_induct0
|
changeset |
files
|
| Wed, 20 Aug 2014 20:50:28 +0200 |
wenzelm |
added jdk-8u20 (inactive);
|
changeset |
files
|
| Wed, 20 Aug 2014 17:30:43 +0200 |
wenzelm |
proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
|
changeset |
files
|
| Wed, 20 Aug 2014 17:23:47 +0200 |
wenzelm |
support for declaration within token source;
|
changeset |
files
|
| Wed, 20 Aug 2014 16:06:10 +0200 |
wenzelm |
more uniform data slot;
|
changeset |
files
|
| Wed, 20 Aug 2014 15:12:32 +0200 |
wenzelm |
default command position is only valid for default text chunk (amending dcb758188aa6);
|
changeset |
files
|
| Wed, 20 Aug 2014 11:54:17 +0200 |
wenzelm |
tuned -- more total;
|
changeset |
files
|
| Wed, 20 Aug 2014 11:51:39 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 20 Aug 2014 11:05:41 +0200 |
wenzelm |
support for nested Token.src within Token.T;
|
changeset |
files
|
| Tue, 19 Aug 2014 23:17:51 +0200 |
wenzelm |
tuned signature -- moved type src to Token, without aliases;
|
changeset |
files
|
| Tue, 19 Aug 2014 18:21:29 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 19 Aug 2014 18:11:04 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Tue, 19 Aug 2014 17:00:44 +0200 |
wenzelm |
added PARALLEL_ALLGOALS convenience;
|
changeset |
files
|
| Tue, 19 Aug 2014 16:46:07 +0200 |
wenzelm |
just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
|
changeset |
files
|
| Tue, 19 Aug 2014 16:09:11 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 19 Aug 2014 15:55:06 +0200 |
wenzelm |
more compact datatypes;
|
changeset |
files
|
| Tue, 19 Aug 2014 15:10:37 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 19 Aug 2014 14:51:25 +0200 |
wenzelm |
clarifed Method.evaluate: turn text into semantic method (like Basic);
|
changeset |
files
|
| Tue, 19 Aug 2014 12:05:11 +0200 |
wenzelm |
simplified type Proof.method;
|
changeset |
files
|
| Mon, 18 Aug 2014 15:46:27 +0200 |
wenzelm |
more general dummy: may contain "parked arguments", for example;
|
changeset |
files
|
| Tue, 19 Aug 2014 16:46:33 +0200 |
desharna |
document 'ctr_transfer'
|
changeset |
files
|
| Tue, 19 Aug 2014 16:46:31 +0200 |
desharna |
generate 'ctr_transfer' for (co)datatypes
|
changeset |
files
|
| Tue, 19 Aug 2014 15:19:16 +0200 |
Andreas Lochbihler |
rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup
|
changeset |
files
|
| Tue, 19 Aug 2014 14:58:38 +0200 |
Andreas Lochbihler |
Enum.finite_5 already provides a non-distributive lattice (see 51aa30c9ee4e)
|
changeset |
files
|
| Tue, 19 Aug 2014 09:39:11 +0200 |
blanchet |
reduced dependency on 'Datatype' theory and ML module
|
changeset |
files
|
| Tue, 19 Aug 2014 09:36:57 +0200 |
blanchet |
removed Z3 3.2, now superseded by Z3 4.3
|
changeset |
files
|
| Tue, 19 Aug 2014 09:36:37 +0200 |
blanchet |
avoid old 'smt' method in examples
|
changeset |
files
|
| Tue, 19 Aug 2014 09:34:57 +0200 |
blanchet |
robustified tactics
|
changeset |
files
|
| Tue, 19 Aug 2014 09:34:41 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 19 Aug 2014 09:34:30 +0200 |
blanchet |
don't note low-level (co)datatype theorems, unless 'bnf_note_all' is set
|
changeset |
files
|
| Tue, 19 Aug 2014 09:34:27 +0200 |
blanchet |
documented slight incompatibility in NEWS
|
changeset |
files
|
| Mon, 18 Aug 2014 19:18:08 +0200 |
blanchet |
removed junk
|
changeset |
files
|
| Mon, 18 Aug 2014 19:16:51 +0200 |
blanchet |
updated docs
|
changeset |
files
|
| Mon, 18 Aug 2014 19:16:30 +0200 |
blanchet |
set attributes on 'set_cases' theorem
|
changeset |
files
|
| Mon, 18 Aug 2014 18:48:39 +0200 |
blanchet |
cleaned up derivation of 'sset_induct'
|
changeset |
files
|
| Mon, 18 Aug 2014 17:20:14 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 18 Aug 2014 17:20:13 +0200 |
blanchet |
added collection theorem for consistency and convenience
|
changeset |
files
|
| Mon, 18 Aug 2014 17:19:58 +0200 |
blanchet |
reordered some (co)datatype property names for more consistency
|
changeset |
files
|
| Mon, 18 Aug 2014 15:03:25 +0200 |
desharna |
document 'map_cong_simp'
|
changeset |
files
|
| Mon, 18 Aug 2014 15:03:22 +0200 |
desharna |
generate 'map_cong_simp' for BNFs
|
changeset |
files
|
| Mon, 18 Aug 2014 14:19:23 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 18 Aug 2014 13:19:04 +0200 |
wenzelm |
merged;
|
changeset |
files
|
| Mon, 18 Aug 2014 12:17:31 +0200 |
wenzelm |
Added tag Isabelle2014-RC4 for changeset 113b43b84412
Isabelle2014
|
changeset |
files
|
| Mon, 18 Aug 2014 12:15:11 +0200 |
wenzelm |
updated to jdk-7u67;
|
changeset |
files
|
| Sun, 17 Aug 2014 16:05:43 +0200 |
wenzelm |
postpone changes in intermediate state between remove_versions/removed_versions, which is important for handle_change to refer to defined items on prover side;
|
changeset |
files
|
| Fri, 15 Aug 2014 13:39:59 +0200 |
wenzelm |
explicit system message for protocol failure -- show on Syslog panel instead of Raw Output;
|
changeset |
files
|
| Wed, 13 Aug 2014 20:21:04 +0200 |
wenzelm |
added option editor_syslog_limit;
|
changeset |
files
|
| Wed, 13 Aug 2014 20:08:29 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 13 Aug 2014 15:45:41 +0200 |
wenzelm |
updated to cygwin-20140813 -- some version after 1.7.31-3;
|
changeset |
files
|
| Mon, 18 Aug 2014 14:09:21 +0200 |
desharna |
document 'inj_map_strong'
|
changeset |
files
|
| Mon, 18 Aug 2014 14:09:09 +0200 |
desharna |
generate 'inj_map_strong' for BNFs
|
changeset |
files
|
| Mon, 18 Aug 2014 13:49:47 +0200 |
desharna |
note 'inj_map' more often
|
changeset |
files
|
| Mon, 18 Aug 2014 13:46:26 +0200 |
desharna |
generate property 'rel_mono_strong' for BNFs
|
changeset |
files
|
| Mon, 18 Aug 2014 13:46:22 +0200 |
desharna |
renamed 'rel_mono_strong' to 'rel_mono_strong0'
|
changeset |
files
|
| Sun, 17 Aug 2014 22:27:58 +0200 |
blanchet |
use 'image_mset' as BNF map function
|
changeset |
files
|
| Sun, 17 Aug 2014 16:24:04 +0200 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Sat, 16 Aug 2014 22:14:57 +0200 |
wenzelm |
updated to named_theorems;
|
changeset |
files
|
| Sat, 16 Aug 2014 21:11:08 +0200 |
wenzelm |
updated to named_theorems;
|
changeset |
files
|
| Sat, 16 Aug 2014 20:46:59 +0200 |
wenzelm |
updated to named_theorems;
|
changeset |
files
|
| Sat, 16 Aug 2014 20:27:51 +0200 |
wenzelm |
updated to named_theorems;
|
changeset |
files
|
| Sat, 16 Aug 2014 20:14:45 +0200 |
wenzelm |
updated to named_theorems;
|
changeset |
files
|
| Sat, 16 Aug 2014 19:20:11 +0200 |
wenzelm |
updated to named_theorems;
|
changeset |
files
|
| Sat, 16 Aug 2014 19:01:31 +0200 |
wenzelm |
clarified order of rules;
|
changeset |
files
|
| Sat, 16 Aug 2014 18:31:47 +0200 |
wenzelm |
updated to named_theorems;
|
changeset |
files
|
| Sat, 16 Aug 2014 18:08:55 +0200 |
wenzelm |
updated to named_theorems;
|
changeset |
files
|
| Sat, 16 Aug 2014 16:45:39 +0200 |
wenzelm |
clarified order of arith rules;
|
changeset |
files
|
| Sat, 16 Aug 2014 16:18:39 +0200 |
wenzelm |
clarified order of rules for match_tac/resolve_tac;
|
changeset |
files
|
| Sat, 16 Aug 2014 14:42:35 +0200 |
wenzelm |
updated to named_theorems;
|
changeset |
files
|
| Sat, 16 Aug 2014 14:32:26 +0200 |
wenzelm |
updated to named_theorems;
|
changeset |
files
|
| Sat, 16 Aug 2014 14:27:41 +0200 |
wenzelm |
updated to named_theorems;
|
changeset |
files
|
| Sat, 16 Aug 2014 14:12:39 +0200 |
wenzelm |
updated to named_theorems;
|
changeset |
files
|
| Sat, 16 Aug 2014 13:54:19 +0200 |
wenzelm |
updated to named_theorems;
|
changeset |
files
|
| Sat, 16 Aug 2014 13:23:50 +0200 |
wenzelm |
modernized module name and setup;
|
changeset |
files
|
| Sat, 16 Aug 2014 12:15:56 +0200 |
wenzelm |
updated syntax for localized commands;
|
changeset |
files
|
| Sat, 16 Aug 2014 12:10:36 +0200 |
wenzelm |
updated documentation concerning 'named_theorems';
|
changeset |
files
|
| Sat, 16 Aug 2014 11:35:33 +0200 |
wenzelm |
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
|
changeset |
files
|
| Fri, 15 Aug 2014 18:02:34 +0200 |
wenzelm |
more informative Token.Name with history of morphisms;
|
changeset |
files
|
| Thu, 14 Aug 2014 19:55:00 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 14 Aug 2014 16:20:14 +0200 |
wenzelm |
more informative Token.Fact: retain name of dynamic fact (without selection);
|
changeset |
files
|
| Thu, 14 Aug 2014 14:28:11 +0200 |
wenzelm |
localized command 'method_setup' and 'attribute_setup';
|
changeset |
files
|
| Thu, 14 Aug 2014 12:49:49 +0200 |
wenzelm |
T1 font encoding with searchable underscore (requires proper cm-super fonts);
|
changeset |
files
|
| Thu, 14 Aug 2014 12:46:37 +0200 |
wenzelm |
prefer high-level change of \isabellestyle;
|
changeset |
files
|
| Thu, 14 Aug 2014 12:33:21 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 14 Aug 2014 12:13:24 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 14 Aug 2014 11:55:09 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 14 Aug 2014 11:51:17 +0200 |
wenzelm |
localized method definitions (see also f14c1248d064);
|
changeset |
files
|
| Thu, 14 Aug 2014 10:48:40 +0200 |
wenzelm |
tuned signature -- prefer self-contained user-space tool;
|
changeset |
files
|
| Thu, 14 Aug 2014 13:21:19 +0200 |
desharna |
document property 'rel_map'
|
changeset |
files
|
| Thu, 14 Aug 2014 13:20:54 +0200 |
desharna |
generate 'rel_map' theorem for BNFs
|
changeset |
files
|
| Wed, 13 Aug 2014 22:29:43 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 13 Aug 2014 20:43:19 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 13 Aug 2014 16:06:32 +0200 |
wenzelm |
tuned signature -- proper Local_Theory.add_thms_dynamic;
|
changeset |
files
|
| Wed, 13 Aug 2014 14:57:03 +0200 |
wenzelm |
transfer result of Global_Theory.add_thms_dynamic to context stack;
|
changeset |
files
|
| Wed, 13 Aug 2014 13:57:55 +0200 |
wenzelm |
localized attribute definitions;
|
changeset |
files
|
| Wed, 13 Aug 2014 13:30:28 +0200 |
wenzelm |
load local_theory.ML before attrib.ML, with subtle change of semantics due to canonical Local_Theory.map_contexts instead of private Local_Theory.map_top;
|
changeset |
files
|
| Wed, 13 Aug 2014 12:59:27 +0200 |
wenzelm |
clarified terminology: first is top (amending d110b0d1bc12);
|
changeset |
files
|
| Wed, 13 Aug 2014 12:52:26 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Wed, 13 Aug 2014 10:46:14 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Wed, 13 Aug 2014 17:17:51 +0200 |
Andreas Lochbihler |
add algebraic type class instances for Enum.finite* types
|
changeset |
files
|
| Wed, 13 Aug 2014 14:57:16 +0200 |
Andreas Lochbihler |
Quickcheck_Types is no longer needed due to 51aa30c9ee4e
|
changeset |
files
|
| Tue, 12 Aug 2014 21:29:50 +0200 |
wenzelm |
clarified focus and key handling -- more like SideKick;
|
changeset |
files
|
| Tue, 12 Aug 2014 20:42:39 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 12 Aug 2014 20:18:27 +0200 |
wenzelm |
tuned signature according to Scala version -- prefer explicit argument;
|
changeset |
files
|
| Tue, 12 Aug 2014 18:54:53 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 12 Aug 2014 18:36:43 +0200 |
wenzelm |
generic process wrapping in Prover;
|
changeset |
files
|
| Tue, 12 Aug 2014 17:28:07 +0200 |
wenzelm |
more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;
|
changeset |
files
|
| Tue, 12 Aug 2014 16:20:09 +0200 |
wenzelm |
allow hyperlinks without offset, just in case the prover emits such reports, despite Position.is_reported;
|
changeset |
files
|
| Tue, 12 Aug 2014 16:10:59 +0200 |
wenzelm |
more frugal standard message properties;
|
changeset |
files
|
| Tue, 12 Aug 2014 15:46:20 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 12 Aug 2014 15:31:24 +0200 |
wenzelm |
clarified Position.Identified: do not require range from prover, default to command position;
|
changeset |
files
|
| Tue, 12 Aug 2014 14:15:58 +0200 |
wenzelm |
maintain Command_Range position as in ML;
|
changeset |
files
|
| Tue, 12 Aug 2014 13:18:17 +0200 |
wenzelm |
more compact representation of special string values;
|
changeset |
files
|
| Tue, 12 Aug 2014 12:06:22 +0200 |
wenzelm |
separate Java FX modules -- no need to include jfxrt.jar by default;
|
changeset |
files
|
| Tue, 12 Aug 2014 00:23:30 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 12 Aug 2014 00:17:02 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 12 Aug 2014 00:08:32 +0200 |
wenzelm |
separate module Command_Span: mostly syntactic representation;
|
changeset |
files
|
| Mon, 11 Aug 2014 22:59:38 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 11 Aug 2014 22:46:27 +0200 |
wenzelm |
clarified Command_Span in accordance to Scala (see also c2c1e5944536);
|
changeset |
files
|
| Mon, 11 Aug 2014 22:43:26 +0200 |
wenzelm |
tuned output, in accordance to transaction name in ML;
|
changeset |
files
|
| Mon, 11 Aug 2014 22:29:48 +0200 |
wenzelm |
more explicit type Span in Scala, according to ML version;
|
changeset |
files
|
| Mon, 11 Aug 2014 20:46:56 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Mon, 11 Aug 2014 20:30:01 +0200 |
wenzelm |
clarified signature: entity serial number is not position id;
|
changeset |
files
|
| Tue, 12 Aug 2014 17:18:12 +0200 |
blanchet |
avoid needless (and wrong w.r.t. sorts) generation of type variables; tuned whitespaces;
|
changeset |
files
|
| Tue, 12 Aug 2014 15:48:59 +0200 |
blanchet |
improved unfolding of 'let's
|
changeset |
files
|
| Tue, 12 Aug 2014 15:48:59 +0200 |
blanchet |
tuned whitespace
|
changeset |
files
|
| Tue, 12 Aug 2014 15:48:59 +0200 |
blanchet |
less aggressive unfolding; removed debugging;
|
changeset |
files
|
| Tue, 12 Aug 2014 12:32:05 +0200 |
desharna |
document property 'set_cases'
|
changeset |
files
|
| Tue, 12 Aug 2014 12:31:42 +0200 |
desharna |
generate 'set_cases' theorem for (co)datatypes
|
changeset |
files
|
| Tue, 12 Aug 2014 12:01:38 +0200 |
desharna |
document property 'set_intros'
|
changeset |
files
|
| Tue, 12 Aug 2014 12:01:37 +0200 |
desharna |
generate 'set_intros' theorem for (co)datatypes
|
changeset |
files
|
| Mon, 11 Aug 2014 10:43:03 +0200 |
traytel |
use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
|
changeset |
files
|
| Sun, 10 Aug 2014 20:45:48 +0200 |
wenzelm |
reduced warnings;
|
changeset |
files
|
| Sun, 10 Aug 2014 19:53:30 +0200 |
wenzelm |
some localization;
|
changeset |
files
|
| Sun, 10 Aug 2014 19:44:20 +0200 |
wenzelm |
support aliases within the facts space;
|
changeset |
files
|
| Sun, 10 Aug 2014 16:13:12 +0200 |
wenzelm |
support for named collections of theorems in canonical order;
|
changeset |
files
|
| Sun, 10 Aug 2014 15:59:12 +0200 |
wenzelm |
insist in proper 'document_files';
|
changeset |
files
|
| Sun, 10 Aug 2014 15:45:06 +0200 |
wenzelm |
tuned -- avoid confusion with @{assert} for system failures (exception Fail);
|
changeset |
files
|
| Sun, 10 Aug 2014 15:16:01 +0200 |
wenzelm |
tuned -- eliminated redundant check (see 1f77110c94ef);
|
changeset |
files
|
| Sun, 10 Aug 2014 14:34:43 +0200 |
wenzelm |
merged -- with manual conflict resolution for src/HOL/SMT_Examples/SMT_Examples.certs2, src/HOL/SMT_Examples/SMT_Word_Examples.certs2, src/Doc/Prog_Prove/document/intro-isabelle.tex;
|
changeset |
files
|
| Sun, 10 Aug 2014 14:31:06 +0200 |
wenzelm |
updated URL (anticipate merge with 85b8cc142384);
|
changeset |
files
|
| Sun, 10 Aug 2014 14:08:36 +0200 |
wenzelm |
Added tag Isabelle2014-RC3 for changeset 91e188508bc9
|
changeset |
files
|
| Sun, 10 Aug 2014 13:59:08 +0200 |
wenzelm |
proper layered_pane for JDialog, e.g. relevant for floating dockables in jEdit, for completion popup in text field;
|
changeset |
files
|
| Sun, 10 Aug 2014 13:06:26 +0200 |
wenzelm |
follow link to originating command, to ensure that Simplifier_Trace_Dockable displays its results (via current_command);
|
changeset |
files
|
| Sat, 09 Aug 2014 18:50:39 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 09 Aug 2014 14:16:46 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 09 Aug 2014 14:11:01 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 09 Aug 2014 11:43:58 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Sat, 09 Aug 2014 11:25:46 +0200 |
wenzelm |
clarified synchronized scope;
|
changeset |
files
|
| Sat, 09 Aug 2014 11:18:01 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Fri, 08 Aug 2014 22:05:02 +0200 |
wenzelm |
application manifest for Windows 8/8.1 dpi scaling;
|
changeset |
files
|
| Fri, 08 Aug 2014 20:17:13 +0200 |
wenzelm |
observe context visibility -- less redundant warnings;
|
changeset |
files
|
| Fri, 08 Aug 2014 11:43:08 +0200 |
wenzelm |
improved monitor panel;
|
changeset |
files
|
| Tue, 05 Aug 2014 23:52:56 +0200 |
wenzelm |
protocol command for heap management, e.g. in Isabelle/jEdit/Scala console: PIDE.session.protocol_command("ML_System.share_common_data");
|
changeset |
files
|
| Tue, 05 Aug 2014 20:40:35 +0200 |
wenzelm |
added system option editor_output_delay: lower value might help big sessions under low-memory situations;
|
changeset |
files
|
| Tue, 05 Aug 2014 19:58:07 +0200 |
wenzelm |
obsolete (see f7700146678d);
|
changeset |
files
|
| Tue, 05 Aug 2014 16:58:19 +0200 |
wenzelm |
tuned proofs -- fewer warnings;
|
changeset |
files
|
| Tue, 05 Aug 2014 16:21:27 +0200 |
wenzelm |
clarified Element.init vs. Element.init' -- the latter also avoids redundant warnings due to declatations when preparing locale expressions / interpretations;
|
changeset |
files
|
| Tue, 05 Aug 2014 15:07:11 +0200 |
wenzelm |
avoid duplication of warnings stemming from simp/intro declarations etc.;
|
changeset |
files
|
| Tue, 05 Aug 2014 12:56:15 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Tue, 05 Aug 2014 12:42:38 +0200 |
wenzelm |
restrict edit_command (for sendback) to current node -- no attempt to goto target buffer first, which might not be loaded;
|
changeset |
files
|
| Tue, 05 Aug 2014 12:14:25 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 05 Aug 2014 12:01:32 +0200 |
wenzelm |
more careful treatment of context visibility for rule declarations (see also 39d9c7f175e0, e639d91d9073) -- avoid duplicate warnings;
|
changeset |
files
|
| Tue, 05 Aug 2014 11:06:36 +0200 |
wenzelm |
refined context visibility again (amending f5f9fad3321c, 8e3e004f1c31): avoid spurious warning due to global config options;
|
changeset |
files
|
| Mon, 04 Aug 2014 19:47:25 +0200 |
wenzelm |
even more thorough reset on mouse drag (see also 0c63f3538639, 7e8c11011fdf);
|
changeset |
files
|
| Mon, 04 Aug 2014 17:55:11 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 04 Aug 2014 17:53:17 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 04 Aug 2014 10:48:35 +0200 |
wenzelm |
Added tag Isabelle2014-RC2 for changeset ee908fccabc2
|
changeset |
files
|
| Mon, 04 Aug 2014 10:47:26 +0200 |
wenzelm |
more user aliases;
|
changeset |
files
|
| Mon, 04 Aug 2014 07:31:27 +0200 |
noschinl |
registered Haskabelle-2014
|
changeset |
files
|
| Fri, 01 Aug 2014 13:59:34 +0200 |
Lars Noschinski |
tuned, so codegen runs with current isabelle again
|
changeset |
files
|
| Sun, 03 Aug 2014 17:38:59 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Sun, 03 Aug 2014 17:33:38 +0200 |
wenzelm |
more robust popup geometry vs. formatted margin;
|
changeset |
files
|
| Sun, 03 Aug 2014 17:17:59 +0200 |
wenzelm |
tuned message;
|
changeset |
files
|
| Sat, 02 Aug 2014 23:20:49 +0200 |
wenzelm |
updated URL;
|
changeset |
files
|
| Sat, 02 Aug 2014 21:22:28 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 02 Aug 2014 20:58:15 +0200 |
wenzelm |
updated URL;
|
changeset |
files
|
| Sat, 02 Aug 2014 19:38:32 +0200 |
wenzelm |
more emphatic warning via error_message (violating historic TTY protocol);
|
changeset |
files
|
| Sat, 02 Aug 2014 19:29:02 +0200 |
wenzelm |
proper priority for error over warning also for node_status (see 9c5220e05e04);
|
changeset |
files
|
| Sat, 02 Aug 2014 16:35:59 +0200 |
wenzelm |
more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);
|
changeset |
files
|
| Sat, 02 Aug 2014 12:24:30 +0200 |
wenzelm |
always resolve symlinks for local files, e.g. relevant for ML_file to load proper source via editor instead of stored file via prover;
|
changeset |
files
|
| Sat, 02 Aug 2014 11:39:13 +0200 |
wenzelm |
tuned output;
|
changeset |
files
|
| Fri, 01 Aug 2014 22:52:53 +0200 |
wenzelm |
prefer non-strict Execution.print, e.g relevant for redirected ML compiler reports after error (see also e79f76a48449 and 40274e4f5ebf);
|
changeset |
files
|
| Fri, 01 Aug 2014 15:08:49 +0200 |
blanchet |
careful when calling 'Thm.proof_body_of' -- it can throw exceptions
|
changeset |
files
|
| Fri, 01 Aug 2014 20:43:23 +0200 |
wenzelm |
removed unused stuff;
|
changeset |
files
|
| Fri, 01 Aug 2014 20:20:17 +0200 |
wenzelm |
agree on keyword categories with ML;
|
changeset |
files
|
| Fri, 01 Aug 2014 20:15:00 +0200 |
wenzelm |
more keyword categories (as in ML);
|
changeset |
files
|
| Thu, 31 Jul 2014 22:02:21 +0200 |
wenzelm |
prefer dynamic ML_print_depth if context happens to be available;
|
changeset |
files
|
| Thu, 31 Jul 2014 21:29:31 +0200 |
wenzelm |
completion popup supports both ENTER and TAB (default);
|
changeset |
files
|
| Thu, 31 Jul 2014 20:59:10 +0200 |
wenzelm |
clarified compile-time use of ML_print_depth;
|
changeset |
files
|
| Thu, 31 Jul 2014 20:09:30 +0200 |
wenzelm |
more general notion of "user error" including empty message -- NB: Output.error_message needs non-empty string to emit anything;
|
changeset |
files
|
| Wed, 30 Jul 2014 09:40:28 +0200 |
blanchet |
correctly resolve selector names in default value equations
|
changeset |
files
|
| Wed, 30 Jul 2014 16:44:54 +0200 |
kuncar |
update documentation for Lifting/Transfer
|
changeset |
files
|
| Wed, 30 Jul 2014 16:44:54 +0200 |
kuncar |
add Isabelle Datatype Manual to the bibliography
|
changeset |
files
|
| Wed, 30 Jul 2014 21:40:19 +0200 |
wenzelm |
CONTRIBUTORS;
|
changeset |
files
|
| Wed, 30 Jul 2014 16:44:54 +0200 |
kuncar |
NEWS
|
changeset |
files
|
| Tue, 29 Jul 2014 17:13:25 +0200 |
hoelzl |
better ordering of positive_integral renaming to nn_integral in NEWS
|
changeset |
files
|
| Mon, 28 Jul 2014 12:31:30 +0200 |
desharna |
made tactic more robust w.r.t. dead variables; tuned;
|
changeset |
files
|
| Sun, 27 Jul 2014 21:20:11 +0200 |
blanchet |
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
|
changeset |
files
|
| Mon, 28 Jul 2014 11:03:28 +0200 |
wenzelm |
some actual workaround to remove document nodes;
|
changeset |
files
|
| Sun, 27 Jul 2014 15:40:19 +0200 |
wenzelm |
Added tag Isabelle2014-RC1 for changeset c0fd03d13d28
|
changeset |
files
|
| Sat, 09 Aug 2014 21:03:42 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 09 Aug 2014 07:59:15 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Fri, 08 Aug 2014 17:36:08 +0200 |
Andreas Lochbihler |
add complete_lattice instances for Enum.finite_* types such that quickcheck deals with lattice class operations
|
changeset |
files
|
| Fri, 08 Aug 2014 08:26:32 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
|
changeset |
files
|
| Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
generate nicer 'set' theorems for (co)datatypes
|
changeset |
files
|
| Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
compile
|
changeset |
files
|
| Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
took out test driver
|
changeset |
files
|
| Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
make TPTP tools work on polymorphic (TFF1) problems as well
|
changeset |
files
|
| Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
put comments between TPTP lines to comply with TPTP BNF
|
changeset |
files
|
| Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
test driver
|
changeset |
files
|
| Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
treat variables as frees in 'conjecture's
|
changeset |
files
|
| Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
support TFF1 in TPTP parser/interpreter
|
changeset |
files
|
| Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 07 Aug 2014 09:35:31 +0200 |
traytel |
tuned
|
changeset |
files
|
| Thu, 07 Aug 2014 10:06:18 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Thu, 07 Aug 2014 09:48:04 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Wed, 06 Aug 2014 18:20:31 +0200 |
traytel |
merged
|
changeset |
files
|
| Wed, 06 Aug 2014 16:00:11 +0200 |
traytel |
handle deep nesting in N2M
|
changeset |
files
|
| Wed, 06 Aug 2014 10:20:50 +0200 |
traytel |
made tactic more robust
|
changeset |
files
|
| Wed, 06 Aug 2014 18:03:43 +0200 |
nipkow |
added lemma
|
changeset |
files
|
| Wed, 06 Aug 2014 08:18:35 +0200 |
nipkow |
replaced misleading - by _
|
changeset |
files
|
| Tue, 05 Aug 2014 20:25:12 +0200 |
blanchet |
more correct clique computation for N2M
|
changeset |
files
|
| Tue, 05 Aug 2014 15:55:39 +0200 |
blanchet |
regenerated ML-Lex/Yacc files
|
changeset |
files
|
| Tue, 05 Aug 2014 15:54:47 +0200 |
blanchet |
correctly interpret arithmetic types
|
changeset |
files
|
| Tue, 05 Aug 2014 14:02:47 +0200 |
blanchet |
added 'datatype_compat' tests
|
changeset |
files
|
| Tue, 05 Aug 2014 13:52:35 +0200 |
blanchet |
tuning whitespace
|
changeset |
files
|
| Tue, 05 Aug 2014 11:07:53 +0200 |
blanchet |
tuned skolemization
|
changeset |
files
|
| Tue, 05 Aug 2014 10:59:40 +0200 |
blanchet |
rationalize Skolem names
|
changeset |
files
|
| Tue, 05 Aug 2014 10:17:15 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 05 Aug 2014 10:02:35 +0200 |
blanchet |
tuned code
|
changeset |
files
|
| Tue, 05 Aug 2014 09:58:23 +0200 |
blanchet |
don't rename variables which will be renamed later anyway
|
changeset |
files
|
| Tue, 05 Aug 2014 09:55:42 +0200 |
blanchet |
normalize skolem argument variable names so that they coincide when taking the conjunction
|
changeset |
files
|
| Tue, 05 Aug 2014 09:20:00 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 04 Aug 2014 16:55:03 +0200 |
blanchet |
tuned comments
|
changeset |
files
|
| Mon, 04 Aug 2014 16:53:09 +0200 |
blanchet |
deal with E definitions
|
changeset |
files
|
| Mon, 04 Aug 2014 15:08:13 +0200 |
blanchet |
updated 'compress' docs
|
changeset |
files
|
| Mon, 04 Aug 2014 15:02:02 +0200 |
blanchet |
cleaner 'compress' option
|
changeset |
files
|
| Mon, 04 Aug 2014 14:19:43 +0200 |
blanchet |
renamed 'sh_minimize' to 'minimize'; compile;
|
changeset |
files
|
| Mon, 04 Aug 2014 13:48:05 +0200 |
blanchet |
restored more sorting
|
changeset |
files
|
| Mon, 04 Aug 2014 13:16:18 +0200 |
blanchet |
tuned terminology (cf. 'isar_proofs' option)
|
changeset |
files
|
| Mon, 04 Aug 2014 13:13:10 +0200 |
blanchet |
sort facts in minimizer as well
|
changeset |
files
|
| Mon, 04 Aug 2014 13:06:24 +0200 |
blanchet |
default on 'metis' for ATPs if preplaying is disabled
|
changeset |
files
|
| Mon, 04 Aug 2014 12:52:48 +0200 |
blanchet |
more informative preplay failures
|
changeset |
files
|
| Mon, 04 Aug 2014 12:28:42 +0200 |
blanchet |
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
|
changeset |
files
|
| Mon, 04 Aug 2014 11:54:23 +0200 |
blanchet |
slightly earlier exit from preplaying
|
changeset |
files
|
| Mon, 04 Aug 2014 11:43:19 +0200 |
blanchet |
honor 'dont_minimize' option when preplaying one-liner proof
|
changeset |
files
|
| Sun, 22 Jun 2014 06:16:57 +0100 |
sultana |
Metis is being used to emulate E steps;
|
changeset |
files
|
| Sun, 22 Jun 2014 06:16:56 +0100 |
sultana |
updated application of print_tac to take context parameter;
|
changeset |
files
|
| Sat, 02 Aug 2014 00:15:08 +0200 |
blanchet |
better duplicate detection
|
changeset |
files
|
| Fri, 01 Aug 2014 23:58:42 +0200 |
blanchet |
normalize conjectures vs. negated conjectures when comparing terms
|
changeset |
files
|
| Fri, 01 Aug 2014 23:33:43 +0200 |
blanchet |
tweaked 'clone' formula detection
|
changeset |
files
|
| Fri, 01 Aug 2014 23:29:50 +0200 |
blanchet |
fine-tuned Isar reconstruction, esp. boolean simplifications
|
changeset |
files
|
| Fri, 01 Aug 2014 23:29:49 +0200 |
blanchet |
centralized boolean simplification so that e.g. LEO-II benefits from it
|
changeset |
files
|
| Fri, 01 Aug 2014 20:44:51 +0200 |
blanchet |
careful when compressing 'obtains'
|
changeset |
files
|
| Fri, 01 Aug 2014 20:44:29 +0200 |
blanchet |
better handling of variable names
|
changeset |
files
|
| Fri, 01 Aug 2014 20:15:41 +0200 |
blanchet |
try to get rid of skolems first
|
changeset |
files
|
| Fri, 01 Aug 2014 20:08:50 +0200 |
blanchet |
nicer generated variable names
|
changeset |
files
|
| Fri, 01 Aug 2014 19:44:18 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 01 Aug 2014 19:36:23 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 01 Aug 2014 19:32:46 +0200 |
blanchet |
no need to 'obtain' variables not in formula
|
changeset |
files
|
| Fri, 01 Aug 2014 19:32:10 +0200 |
blanchet |
more precise handling of LEO-II skolemization
|
changeset |
files
|
| Fri, 01 Aug 2014 16:07:34 +0200 |
blanchet |
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
|
changeset |
files
|
| Fri, 01 Aug 2014 16:07:33 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 01 Aug 2014 16:07:33 +0200 |
blanchet |
peek instead of joining -- is perhaps less risky
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
export ML function
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
compile
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
removed 'metisFT' support in Mirabelle
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
removed Mirabelle minimization code
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
modernized Mirabelle (a bit) and made it compile
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
restored a bit of laziness
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
reorder quantifiers to ease Z3 skolemization
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
tuned order of arguments
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
tuned name context code
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
tuned whitespace
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
more rational unskolemizing of names
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
added appropriate method for skolemization of Z3 steps to the mix
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
pushing skolems under 'iff' sometimes breaks things further down the proof (as was to be feared)
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
honor 'try0' also for one-liners
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
tentatively took out 'fastforce' from the set of tried methods -- it seems to be largely subsumed and is hard to silence
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
further minimize one-liner
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
eliminated needlessly complex message tail
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
updated NEWS
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
update documentation after removal of 'min' subcommand
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
rationalized preplaying by eliminating (now superfluous) laziness
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
removed proof methods as provers from docs
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
simplified minimization logic
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
remove lambda-lifting related assumptions from generated Isar proofs
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
whitespace tuning
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
remove YXML formatting when parsing backquoted facts supplied manually to Sledgehammer
|
changeset |
files
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
generate backquotes without markup, since this confuses preplay; bump up spying version identifier;
|
changeset |
files
|
| Thu, 31 Jul 2014 13:19:57 +0200 |
traytel |
simplified tactics slightly
|
changeset |
files
|
| Thu, 31 Jul 2014 00:45:55 +0200 |
blanchet |
cascading timeout in parallel evaluation, to rapidly find optimum
|
changeset |
files
|
| Wed, 30 Jul 2014 23:52:56 +0200 |
blanchet |
put faster proof methods first
|
changeset |
files
|
| Wed, 30 Jul 2014 23:52:56 +0200 |
blanchet |
use parallel preplay machinery also for one-line proofs
|
changeset |
files
|
| Wed, 30 Jul 2014 23:52:56 +0200 |
blanchet |
updated docs
|
changeset |
files
|
| Wed, 30 Jul 2014 23:52:56 +0200 |
blanchet |
always minimize Sledgehammer results by default
|
changeset |
files
|
| Wed, 30 Jul 2014 23:52:56 +0200 |
blanchet |
tuned ML function name
|
changeset |
files
|
| Wed, 30 Jul 2014 23:52:56 +0200 |
blanchet |
reduced preplay timeout to 1 s
|
changeset |
files
|
| Wed, 30 Jul 2014 23:52:56 +0200 |
blanchet |
added more proof methods for one-liners
|
changeset |
files
|
| Wed, 30 Jul 2014 23:52:56 +0200 |
blanchet |
unlift before uncombine, because the definition of a lambda-lifted symbol might have an SK combinator in it (in hybrid encodings)
|
changeset |
files
|
| Wed, 30 Jul 2014 14:03:58 +0200 |
fleury |
Improving robustness and indentation corrections.
|
changeset |
files
|
| Wed, 30 Jul 2014 14:03:13 +0200 |
fleury |
Skolemization for tmp_ite_elim rule in the SMT solver veriT.
|
changeset |
files
|
| Wed, 30 Jul 2014 14:03:13 +0200 |
fleury |
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
|
changeset |
files
|
| Wed, 30 Jul 2014 14:03:13 +0200 |
fleury |
Whitespace and indentation correction.
|
changeset |
files
|
| Wed, 30 Jul 2014 14:03:13 +0200 |
fleury |
Simplifying the labels in the proof of the SMT solver veriT.
|
changeset |
files
|
| Wed, 30 Jul 2014 14:03:13 +0200 |
fleury |
Changing ~ into - for unuary minus (not supported by veriT)
|
changeset |
files
|
| Wed, 30 Jul 2014 14:03:13 +0200 |
fleury |
imported patch satallax_skolemization_in_tree_part
|
changeset |
files
|
| Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
imported patch hilbert_choice_support
|
changeset |
files
|
| Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
veriT changes for lifted terms, and ite_elim rules.
|
changeset |
files
|
| Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
imported patch satallax_proof_support_Sledgehammer
|
changeset |
files
|
| Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
Basic support for the higher-order ATP Satallax.
|
changeset |
files
|
| Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
Subproofs for the SMT solver veriT.
|
changeset |
files
|
| Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
Basic support for the SMT prover veriT.
|
changeset |
files
|
| Wed, 30 Jul 2014 14:03:11 +0200 |
fleury |
removing the '= True' generated by Leo-II.
|
changeset |
files
|
| Wed, 30 Jul 2014 14:03:11 +0200 |
fleury |
Skolemization support for leo-II and Zipperposition.
|
changeset |
files
|
| Wed, 30 Jul 2014 10:50:30 +0200 |
desharna |
document property 'set_induct'
|
changeset |
files
|
| Wed, 30 Jul 2014 10:50:28 +0200 |
desharna |
generate 'set_induct' theorem for codatatypes
|
changeset |
files
|
| Wed, 30 Jul 2014 00:50:41 +0200 |
blanchet |
also try 'metis' with 'full_types'
|
changeset |
files
|
| Tue, 29 Jul 2014 23:39:35 +0200 |
blanchet |
header tuning
|
changeset |
files
|
| Mon, 28 Jul 2014 10:57:33 +0200 |
blanchet |
correctly translate THF functions from terms to types
|
changeset |
files
|
| Sun, 27 Jul 2014 21:11:35 +0200 |
blanchet |
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
|
changeset |
files
|
| Sun, 27 Jul 2014 15:44:08 +0200 |
wenzelm |
back to post-release mode -- after fork point;
|
changeset |
files
|
| Sun, 27 Jul 2014 15:29:42 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 27 Jul 2014 15:25:00 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 26 Jul 2014 19:19:19 +0200 |
wenzelm |
no -optimise -- produces bad bytecode;
|
changeset |
files
|
| Sat, 26 Jul 2014 14:52:54 +0200 |
wenzelm |
output state first -- avoid fluctuation wrt. warnings, errors, etc.;
|
changeset |
files
|
| Fri, 25 Jul 2014 21:44:03 +0200 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Fri, 25 Jul 2014 21:29:12 +0200 |
wenzelm |
updated to polyml-5.5.2-1 which addresses two hard crashes;
|
changeset |
files
|
| Fri, 25 Jul 2014 20:55:57 +0200 |
wenzelm |
updated to cygwin-20140725, which is presumably close to Cygwin 1.7.31-1;
|
changeset |
files
|
| Fri, 25 Jul 2014 18:41:53 +0200 |
nipkow |
added more functions and lemmas
|
changeset |
files
|
| Fri, 25 Jul 2014 17:13:30 +0200 |
wenzelm |
proper mkdir;
|
changeset |
files
|
| Fri, 25 Jul 2014 16:58:28 +0200 |
wenzelm |
proper option -O;
|
changeset |
files
|
| Fri, 25 Jul 2014 16:50:49 +0200 |
wenzelm |
some reshuffling of Poly/ML version to evade failing tests;
|
changeset |
files
|
| Fri, 25 Jul 2014 15:01:18 +0200 |
wenzelm |
old 'defs' is legacy --- slightly odd side-entry that bypasses regular Local_Theory.define interface;
|
changeset |
files
|
| Fri, 25 Jul 2014 14:47:38 +0200 |
wenzelm |
proper volume name, such that background image is found in /Volumes/Isabelle/.background;
|
changeset |
files
|
| Fri, 25 Jul 2014 14:16:39 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 25 Jul 2014 14:15:02 +0200 |
wenzelm |
tuned message;
|
changeset |
files
|
| Fri, 25 Jul 2014 14:13:19 +0200 |
wenzelm |
setup for drag-and-drop DMG;
|
changeset |
files
|
| Fri, 25 Jul 2014 13:22:37 +0200 |
blanchet |
merge
|
changeset |
files
|
| Fri, 25 Jul 2014 13:15:50 +0200 |
blanchet |
reordered provers
|
changeset |
files
|
| Fri, 25 Jul 2014 12:22:18 +0200 |
blanchet |
compile
|
changeset |
files
|
| Fri, 25 Jul 2014 12:20:48 +0200 |
blanchet |
faster minimization by not adding facts that are already in the simpset
|
changeset |
files
|
| Fri, 25 Jul 2014 11:31:20 +0200 |
blanchet |
added missing facts to proof method
|
changeset |
files
|
| Fri, 25 Jul 2014 11:26:23 +0200 |
blanchet |
don't lose 'minimize' flag before it reaches Isar proof text generation
|
changeset |
files
|
| Fri, 25 Jul 2014 11:26:19 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 25 Jul 2014 11:26:17 +0200 |
blanchet |
avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
|
changeset |
files
|
| Fri, 25 Jul 2014 11:26:11 +0200 |
blanchet |
compile
|
changeset |
files
|
| Fri, 25 Jul 2014 11:26:11 +0200 |
blanchet |
more robustness in Isar proof construction
|
changeset |
files
|
| Fri, 25 Jul 2014 11:26:10 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 24 Jul 2014 23:18:01 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 24 Jul 2014 23:17:26 +0200 |
wenzelm |
more elementary exception handling: evade hard crash of (Runtime.thread true undefined) on Poly/ML 5.5.1 and 5.5.2;
|
changeset |
files
|
| Thu, 24 Jul 2014 23:01:23 +0200 |
blanchet |
tuned code
|
changeset |
files
|
| Thu, 24 Jul 2014 20:21:59 +0200 |
kuncar |
having extra assumptions (typically from a context) means there is no chance to have a valid code equation => skip decoding and registration of the code equations
|
changeset |
files
|
| Thu, 24 Jul 2014 20:21:34 +0200 |
kuncar |
store explicitly quotient types with no_code => more precise registration of code equations
|
changeset |
files
|
| Thu, 24 Jul 2014 19:01:06 +0200 |
blanchet |
don't needlessly regenerate entire file when the time stamps are equal
|
changeset |
files
|
| Thu, 24 Jul 2014 18:53:14 +0200 |
blanchet |
eliminated source of 'DUP's in MaSh
|
changeset |
files
|
| Thu, 24 Jul 2014 18:46:38 +0200 |
blanchet |
fixed sorting (broken since 9cc802a8ab06)
|
changeset |
files
|
| Thu, 24 Jul 2014 18:46:38 +0200 |
blanchet |
reenabled MaSh for Isabelle2014 release (hopefully)
|
changeset |
files
|
| Thu, 24 Jul 2014 18:46:38 +0200 |
blanchet |
beware of duplicate fact names
|
changeset |
files
|
| Thu, 24 Jul 2014 18:46:38 +0200 |
blanchet |
refined filter for ATP steps to avoid 'have True' steps in E proofs
|
changeset |
files
|
| Thu, 24 Jul 2014 18:46:38 +0200 |
blanchet |
filter out 'theory(...)' from dependencies early on
|
changeset |
files
|
| Thu, 24 Jul 2014 18:46:38 +0200 |
blanchet |
introduce fact chaining also under first step
|
changeset |
files
|
| Thu, 24 Jul 2014 18:46:38 +0200 |
blanchet |
'shift_quantors' is not an E skolemization rule (cf. 3ab503b04bdb)
|
changeset |
files
|
| Thu, 24 Jul 2014 17:58:29 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 24 Jul 2014 17:13:26 +0200 |
wenzelm |
proper perl;
|
changeset |
files
|
| Thu, 24 Jul 2014 17:11:40 +0200 |
wenzelm |
less warnings -- ignore potential prover startup/shutdown races;
|
changeset |
files
|
| Thu, 24 Jul 2014 16:21:50 +0200 |
wenzelm |
tuned spelling;
|
changeset |
files
|
| Thu, 24 Jul 2014 15:54:56 +0200 |
wenzelm |
further distinction of Isabelle distribution: alert for identified release candidates;
|
changeset |
files
|
| Thu, 24 Jul 2014 15:13:37 +0200 |
wenzelm |
updated to scala-2.11.2;
|
changeset |
files
|
| Thu, 24 Jul 2014 15:01:17 +0200 |
wenzelm |
clarified file names;
|
changeset |
files
|
| Thu, 24 Jul 2014 14:56:30 +0200 |
wenzelm |
less ambitious isatest, avoid "Exception- InternalError: Backing up too far (32bit) raised while compiling" in polyml-5.4.1;
|
changeset |
files
|
| Thu, 24 Jul 2014 14:08:29 +0200 |
wenzelm |
tuned imports;
|
changeset |
files
|
| Thu, 24 Jul 2014 14:04:55 +0200 |
wenzelm |
proper scope of comments;
|
changeset |
files
|
| Thu, 24 Jul 2014 13:48:00 +0200 |
wenzelm |
make SML/NJ happy;
|
changeset |
files
|
| Thu, 24 Jul 2014 13:01:49 +0200 |
kuncar |
prevent beta-contraction in proving extra assumptions for abs_eq
|
changeset |
files
|
| Thu, 24 Jul 2014 11:54:15 +0200 |
wenzelm |
more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy);
|
changeset |
files
|
| Thu, 24 Jul 2014 11:51:22 +0200 |
wenzelm |
reconfirm continuous checking on startup, to address common trap of disabling it accidentally;
|
changeset |
files
|
| Thu, 24 Jul 2014 11:46:40 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 24 Jul 2014 10:38:46 +0200 |
wenzelm |
less authentic SHA1.digest: trust Scala side on blobs and avoid re-calculation via Foreign Language Interface, which might be a cause of problems;
|
changeset |
files
|
| Thu, 24 Jul 2014 10:22:34 +0200 |
wenzelm |
updated NEWS according to d38a98f496dd (see also bdc2c6b40bf2);
|
changeset |
files
|
| Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
stick to external proofs when invoking E, because they are more detailed and do not merge steps
|
changeset |
files
|
| Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
more robust handling of types for skolems (modeled as Frees)
|
changeset |
files
|
| Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
repaired named derivations
|
changeset |
files
|
| Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
use the noted theorems in 'BNF_Comp'
|
changeset |
files
|
| Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
use the noted theorem whenever possible, also in 'BNF_Def'
|
changeset |
files
|
| Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
use termtab instead of (perhaps overly sensitive) thmtab
|
changeset |
files
|
| Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
|
changeset |
files
|
| Wed, 23 Jul 2014 23:16:44 +0200 |
wenzelm |
tuned message;
|
changeset |
files
|
| Wed, 23 Jul 2014 23:08:22 +0200 |
wenzelm |
added action "isabelle.options" (despite problems with initial window size);
|
changeset |
files
|
| Wed, 23 Jul 2014 21:02:45 +0200 |
wenzelm |
more official Thy_Info.script_thy;
|
changeset |
files
|
| Wed, 23 Jul 2014 21:01:28 +0200 |
wenzelm |
more frugal edits;
|
changeset |
files
|
| Wed, 23 Jul 2014 18:16:04 +0200 |
wenzelm |
enable hires explictly, as seen for other high-end Java applications on the Web;
|
changeset |
files
|
| Wed, 23 Jul 2014 18:14:59 +0200 |
wenzelm |
more markup;
|
changeset |
files
|
| Wed, 23 Jul 2014 18:04:16 +0200 |
wenzelm |
another attempt at more aggressive auto-loading (amending af28fdd50690) -- hidden buffers are now suppressed;
|
changeset |
files
|
| Wed, 23 Jul 2014 16:56:03 +0200 |
wenzelm |
more frugal edits;
|
changeset |
files
|
| Wed, 23 Jul 2014 16:20:07 +0200 |
wenzelm |
more explicit treatment of cleared nodes (removal is implicit);
|
changeset |
files
|
| Wed, 23 Jul 2014 15:32:05 +0200 |
wenzelm |
clarified display;
|
changeset |
files
|
| Wed, 23 Jul 2014 15:11:42 +0200 |
wenzelm |
more workarounds for scalac;
|
changeset |
files
|
| Wed, 23 Jul 2014 15:00:46 +0200 |
wenzelm |
clarified display;
|
changeset |
files
|
| Wed, 23 Jul 2014 14:50:20 +0200 |
wenzelm |
avoid redundant data structure;
|
changeset |
files
|
| Wed, 23 Jul 2014 13:01:30 +0200 |
wenzelm |
more explicit discrimination of empty nodes -- suppress from Theories panel;
|
changeset |
files
|
| Wed, 23 Jul 2014 11:53:34 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 23 Jul 2014 11:22:56 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Wed, 23 Jul 2014 11:19:24 +0200 |
wenzelm |
clarified module name: facilitate alternative GUI frameworks;
|
changeset |
files
|
| Wed, 23 Jul 2014 11:08:24 +0200 |
wenzelm |
proper change of perspective for removed nodes (stemming from closed buffers);
|
changeset |
files
|
| Wed, 23 Jul 2014 10:02:19 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 22 Jul 2014 22:18:50 +0200 |
wenzelm |
some robustification of console output;
|
changeset |
files
|
| Tue, 22 Jul 2014 20:03:52 +0200 |
wenzelm |
updated ErrorList.jar;
|
changeset |
files
|
| Tue, 22 Jul 2014 14:52:35 +0200 |
wenzelm |
discontinued presumable workarounds for extra inter-theory space, which are obsolete since 0e5fa27d3293;
|
changeset |
files
|
| Tue, 22 Jul 2014 14:36:31 +0200 |
wenzelm |
evade problems with MikTeX on Windows;
|
changeset |
files
|
| Tue, 22 Jul 2014 14:03:00 +0200 |
wenzelm |
tuned messages;
|
changeset |
files
|
| Tue, 22 Jul 2014 13:36:51 +0200 |
wenzelm |
support multiple selected print operations instead of slightly odd "menu";
|
changeset |
files
|
| Tue, 22 Jul 2014 12:05:53 +0200 |
wenzelm |
more default imports;
|
changeset |
files
|
| Tue, 22 Jul 2014 11:46:34 +0200 |
wenzelm |
no keyword completion within word context -- especially avoid its odd visual rendering;
|
changeset |
files
|
| Tue, 22 Jul 2014 08:07:47 +0200 |
Andreas Lochbihler |
merged
|
changeset |
files
|
| Mon, 21 Jul 2014 17:57:16 +0200 |
Andreas Lochbihler |
merged
|
changeset |
files
|
| Mon, 21 Jul 2014 17:51:29 +0200 |
Andreas Lochbihler |
add parametricity lemmas
|
changeset |
files
|
| Mon, 21 Jul 2014 17:51:11 +0200 |
Andreas Lochbihler |
add lemma
|
changeset |
files
|
| Mon, 21 Jul 2014 20:57:47 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 21 Jul 2014 20:36:25 +0200 |
wenzelm |
refer to Simplifier Trace panel on first invocation;
|
changeset |
files
|
| Mon, 21 Jul 2014 17:39:20 +0200 |
wenzelm |
removed unused markup (cf. 2f7d91242b99);
|
changeset |
files
|
| Mon, 21 Jul 2014 17:37:22 +0200 |
wenzelm |
regular message to refer to Simplifier Trace panel (unused);
|
changeset |
files
|
| Mon, 21 Jul 2014 16:58:12 +0200 |
wenzelm |
proper Swing buttons instead of active areas within text (by Lars Hupel);
|
changeset |
files
|
| Mon, 21 Jul 2014 16:49:06 +0200 |
wenzelm |
misc tuning and simplification;
|
changeset |
files
|
| Mon, 21 Jul 2014 16:04:45 +0200 |
wenzelm |
clarified "simp_trace_new" and corresponding isar-ref section;
|
changeset |
files
|
| Mon, 21 Jul 2014 15:16:50 +0200 |
wenzelm |
more on "Simplifier trace" (by Lars Hupel);
|
changeset |
files
|
| Mon, 21 Jul 2014 14:24:10 +0200 |
wenzelm |
always complete explicit symbols;
|
changeset |
files
|
| Mon, 21 Jul 2014 13:50:26 +0200 |
wenzelm |
discontinued unfinished attempts at syntactic word context (see 2e1398b484aa, 08a1c860bc12, 7f229b0212fe) -- back to more basic completion of Isabelle2013-2;
|
changeset |
files
|
| Mon, 21 Jul 2014 12:25:54 +0200 |
wenzelm |
updated to jdk-7u65;
|
changeset |
files
|
| Mon, 21 Jul 2014 18:04:08 +0200 |
traytel |
regression test for datatypes defined in IsaFoR
|
changeset |
files
|
| Mon, 21 Jul 2014 15:23:57 +0200 |
kleing |
ghc mac installation repaired; test back on.
|
changeset |
files
|
| Sun, 20 Jul 2014 22:05:35 +0200 |
wenzelm |
proper condition wrt. ISABELLE_GHC (cf. 8840fa17e17c);
|
changeset |
files
|
| Sun, 20 Jul 2014 20:00:53 +0200 |
wenzelm |
updated to jdk-8u11 (inactive);
|
changeset |
files
|
| Sun, 20 Jul 2014 19:36:46 +0200 |
wenzelm |
avoid delay_load overrun;
|
changeset |
files
|
| Sun, 20 Jul 2014 17:54:01 +0200 |
wenzelm |
provide explicit options file -- avoid multiple Scala/JVM invocation;
|
changeset |
files
|
| Sun, 20 Jul 2014 17:21:14 +0200 |
wenzelm |
check and build Isabelle session for console tool -- avoid multiple Scala/JVM invocation;
|
changeset |
files
|
| Sat, 19 Jul 2014 21:32:54 +0200 |
kleing |
attempt to run without ISABELLE_GHC setting again on mac-poly
|
changeset |
files
|
| Sat, 19 Jul 2014 21:20:38 +0200 |
kleing |
apparently, setting ISABELLE_GHC makes ghc unusable
|
changeset |
files
|
| Sat, 19 Jul 2014 18:30:43 +0200 |
haftmann |
reverse induction over nonempty lists
|
changeset |
files
|
| Sat, 19 Jul 2014 18:30:42 +0200 |
haftmann |
more appropriate postprocessing of rational numbers: extract sign to front of fraction
|
changeset |
files
|
| Sat, 19 Jul 2014 11:20:09 +0200 |
blanchet |
doc fixes (contributed by Christian Sternagel)
|
changeset |
files
|
| Sat, 19 Jul 2014 11:20:09 +0200 |
blanchet |
made SML/NJ happier
|
changeset |
files
|
| Fri, 18 Jul 2014 22:16:03 +0200 |
kleing |
avoid duplicate fact name
|
changeset |
files
|
| Fri, 18 Jul 2014 21:40:11 +0200 |
kleing |
afp-poly runs on macbroy2 (different ghc)
|
changeset |
files
|
| Fri, 18 Jul 2014 14:21:42 +0200 |
nipkow |
reinstated popular add_ac and mult_ac to avoid needless incompatibilities in user space
|
changeset |
files
|
| Fri, 18 Jul 2014 14:03:09 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Thu, 17 Jul 2014 14:55:56 +0200 |
hoelzl |
register tree with datatype_compat ot support QuickCheck
|
changeset |
files
|
| Thu, 17 Jul 2014 10:29:09 +0200 |
desharna |
fix bug caused by bad context
|
changeset |
files
|
| Thu, 17 Jul 2014 10:28:32 +0200 |
desharna |
add mk_Trueprop_mem utility function
|
changeset |
files
|
| Wed, 16 Jul 2014 17:57:27 +0200 |
blanchet |
disabled MaSh for the Isabelle2014 release, due to a couple of issues
|
changeset |
files
|
| Wed, 16 Jul 2014 10:22:06 +0200 |
desharna |
refactor commonly used functions
|
changeset |
files
|
| Wed, 16 Jul 2014 10:13:38 +0200 |
desharna |
document property 'rel_sel'
|
changeset |
files
|
| Wed, 16 Jul 2014 10:13:00 +0200 |
desharna |
generate 'rel_sel' theorem for (co)datatypes
|
changeset |
files
|
| Wed, 16 Jul 2014 10:11:25 +0200 |
desharna |
fix rel_cases
|
changeset |
files
|
| Tue, 15 Jul 2014 17:49:54 +0200 |
blanchet |
made SML/NJ happier
|
changeset |
files
|
| Tue, 15 Jul 2014 11:13:43 +0200 |
kleing |
add ISABELLE_GHC settings for isatest
|
changeset |
files
|
| Mon, 14 Jul 2014 15:39:23 +0200 |
noschinl |
mira.py: building jEdit plugin is required for makeall
|
changeset |
files
|
| Tue, 15 Jul 2014 00:35:07 +0200 |
blanchet |
took out 'rel_cases' for now because of failing tactic
|
changeset |
files
|
| Tue, 15 Jul 2014 00:21:32 +0200 |
blanchet |
record MaSh algorithm in spying data
|
changeset |
files
|
| Tue, 15 Jul 2014 00:21:32 +0200 |
blanchet |
tuned whitespace (also in strings)
|
changeset |
files
|
| Tue, 15 Jul 2014 00:21:32 +0200 |
blanchet |
also learn when 'fact_filter =' is set explicitly
|
changeset |
files
|
| Tue, 15 Jul 2014 00:21:32 +0200 |
blanchet |
no warning in case MaSh is disabled
|
changeset |
files
|
| Tue, 15 Jul 2014 00:21:32 +0200 |
blanchet |
don't generate a 'set-logic' command when generating problems in a non-standard (but Z3-supported) union-of-everything logic
|
changeset |
files
|
| Tue, 15 Jul 2014 00:21:29 +0200 |
blanchet |
no need for 'mash' subdirectory after removal of Python program
|
changeset |
files
|
| Mon, 14 Jul 2014 01:59:23 +0200 |
panny |
fix typo
|
changeset |
files
|
| Mon, 14 Jul 2014 01:35:43 +0200 |
panny |
throw error for bad input
|
changeset |
files
|
| Mon, 14 Jul 2014 01:22:59 +0200 |
panny |
catch "not found" case
|
changeset |
files
|
| Sat, 12 Jul 2014 19:54:04 +0200 |
blanchet |
merge
|
changeset |
files
|
| Sat, 12 Jul 2014 11:31:23 +0200 |
blanchet |
don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
|
changeset |
files
|
| Sat, 12 Jul 2014 11:31:22 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Sat, 12 Jul 2014 11:31:22 +0200 |
blanchet |
made SML/NJ happier
|
changeset |
files
|
| Fri, 11 Jul 2014 15:52:03 +0200 |
Andreas Lochbihler |
reactivate session Quickcheck_Examples
|
changeset |
files
|
| Fri, 11 Jul 2014 15:35:11 +0200 |
Andreas Lochbihler |
adapt and reactivate Quickcheck_Types and add two test cases
|
changeset |
files
|
| Fri, 11 Jul 2014 00:55:46 +0200 |
blanchet |
more docs
|
changeset |
files
|
| Thu, 10 Jul 2014 18:08:21 +0200 |
blanchet |
lambda-lifting for Z3 Isar proofs
|
changeset |
files
|
| Thu, 10 Jul 2014 17:01:23 +0200 |
blanchet |
append instead of prepend lambda-lifted definitions -- this eases reconstruction in veriT (outside repository)
|
changeset |
files
|
| Thu, 10 Jul 2014 14:12:16 +0200 |
blanchet |
avoid loop in 'all_class_pairs' (caused by e.g. loading the 'Ceta' theory and calling Sledgehammer with the two facts 'fun_of_map.cases' and 'Lattices.bounded_lattice_top_class.sup_top_left' with a polymorphic type encoding)
|
changeset |
files
|
| Wed, 09 Jul 2014 18:57:20 +0200 |
nipkow |
merged
|
changeset |
files
|
| Wed, 09 Jul 2014 11:48:21 +0200 |
nipkow |
added lemmas
|
changeset |
files
|
| Wed, 09 Jul 2014 18:48:37 +0200 |
blanchet |
improved docs
|
changeset |
files
|
| Wed, 09 Jul 2014 11:54:01 +0200 |
blanchet |
made SML/NJ happier
|
changeset |
files
|
| Wed, 09 Jul 2014 11:35:52 +0200 |
blanchet |
got rid of a pointer equality
|
changeset |
files
|
| Wed, 09 Jul 2014 11:35:52 +0200 |
blanchet |
get rid of some pointer equalities
|
changeset |
files
|
| Wed, 09 Jul 2014 11:35:52 +0200 |
blanchet |
tuned terminology
|
changeset |
files
|
| Wed, 09 Jul 2014 11:35:52 +0200 |
blanchet |
improvements to the machine learning algos (due to Cezary K.)
|
changeset |
files
|
| Mon, 07 Jul 2014 17:01:11 +0200 |
nipkow |
added lemma
|
changeset |
files
|
| Mon, 07 Jul 2014 16:06:46 +0200 |
desharna |
refactor some tactics
|
changeset |
files
|
| Mon, 07 Jul 2014 16:06:46 +0200 |
desharna |
refactor some tactics
|
changeset |
files
|
| Mon, 07 Jul 2014 16:06:46 +0200 |
desharna |
add helper function map_prod
|
changeset |
files
|
| Mon, 07 Jul 2014 16:06:46 +0200 |
desharna |
document property 'rel_cases'
|
changeset |
files
|
| Mon, 07 Jul 2014 16:06:46 +0200 |
desharna |
generate 'rel_cases' theorem for (co)datatypes
|
changeset |
files
|
| Sat, 05 Jul 2014 20:51:24 +0200 |
wenzelm |
update for release;
|
changeset |
files
|
| Sat, 05 Jul 2014 16:29:19 +0200 |
wenzelm |
Added tag Isabelle2014-RC0 for changeset 251ef0202e71
|
changeset |
files
|
| Sat, 05 Jul 2014 16:28:07 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 05 Jul 2014 13:39:53 +0200 |
wenzelm |
modernized definitions;
|
changeset |
files
|
| Sat, 05 Jul 2014 13:21:53 +0200 |
wenzelm |
proper plain_args to ensure that multi-argument overloading cannot escape pattern restriction (despite more liberal structural containment before 3ae3cc4b1eac);
|
changeset |
files
|
| Sat, 05 Jul 2014 16:07:23 +0200 |
haftmann |
CONTRIBUTORS
|
changeset |
files
|
| Sat, 05 Jul 2014 16:04:23 +0200 |
haftmann |
refrain from auxiliary abbreviation: be more explicit to the reader in situations where syntax translation does not apply;
|
changeset |
files
|
| Sat, 05 Jul 2014 12:04:25 +0200 |
wenzelm |
misc tuning for release;
|
changeset |
files
|
| Sat, 05 Jul 2014 11:19:37 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 05 Jul 2014 11:06:14 +0200 |
haftmann |
NEWS
|
changeset |
files
|
| Sat, 05 Jul 2014 11:01:53 +0200 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
changeset |
files
|
| Sat, 05 Jul 2014 10:09:01 +0200 |
kleing |
added Tom's hyp_subst update
|
changeset |
files
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
changeset |
files
|
| Fri, 04 Jul 2014 20:07:08 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 04 Jul 2014 17:41:35 +0200 |
wenzelm |
insist in explicit overloading;
|
changeset |
files
|
| Fri, 04 Jul 2014 17:19:03 +0200 |
wenzelm |
more uniform names;
|
changeset |
files
|
| Fri, 04 Jul 2014 16:50:57 +0200 |
wenzelm |
misc tuning for release;
|
changeset |
files
|
| Fri, 04 Jul 2014 15:50:28 +0200 |
wenzelm |
revived unchecked theory (see cebaf814ca6e);
|
changeset |
files
|
| Fri, 04 Jul 2014 15:46:13 +0200 |
wenzelm |
suppress completion of obscure keyword;
|
changeset |
files
|
| Fri, 04 Jul 2014 14:58:52 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 04 Jul 2014 14:52:05 +0200 |
wenzelm |
misc tuning for release;
|
changeset |
files
|
| Fri, 04 Jul 2014 11:39:34 +0200 |
wenzelm |
NEWS;
|
changeset |
files
|
| Thu, 03 Jul 2014 16:42:15 +0200 |
nipkow |
Tail recursion no longer supported by "function".
|
changeset |
files
|
| Thu, 03 Jul 2014 14:40:36 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 03 Jul 2014 09:55:16 +0200 |
Christian Sternagel |
weaker assumption for "list_emb_trans"; added lemma
|
changeset |
files
|
| Thu, 03 Jul 2014 09:55:15 +0200 |
Christian Sternagel |
added monotonicity lemma for list embedding
|
changeset |
files
|
| Thu, 03 Jul 2014 09:55:15 +0200 |
Christian Sternagel |
no built-in reflexivity of list embedding (which is more standard; now embedding is reflexive whenever the base-order is)
|
changeset |
files
|
| Thu, 03 Jul 2014 09:55:15 +0200 |
Christian Sternagel |
renamed "list_hembeq" into slightly shorter "list_emb"
|
changeset |
files
|
| Thu, 03 Jul 2014 12:17:55 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Thu, 03 Jul 2014 11:31:25 +0200 |
desharna |
merge
|
changeset |
files
|
| Thu, 03 Jul 2014 11:30:23 +0200 |
desharna |
document property 'rel_intros'
|
changeset |
files
|
| Thu, 03 Jul 2014 11:30:02 +0200 |
desharna |
generate 'rel_intros' theorem for (co)datatypes
|
changeset |
files
|
| Wed, 11 Jun 2014 14:24:23 +1000 |
Thomas Sewell |
Hypsubst preserves equality hypotheses
|
changeset |
files
|
| Wed, 02 Jul 2014 17:34:45 +0200 |
wenzelm |
tuned grammar and spelling (cf. 0cf15843b82f);
|
changeset |
files
|
| Wed, 02 Jul 2014 17:01:51 +0200 |
desharna |
document property 'corec_code'
|
changeset |
files
|
| Wed, 02 Jul 2014 17:01:49 +0200 |
desharna |
generate 'corec_code' theorem for codatatypes
|
changeset |
files
|
| Wed, 02 Jul 2014 13:23:11 +0200 |
wenzelm |
modernized definitions;
|
changeset |
files
|
| Wed, 02 Jul 2014 13:06:07 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Wed, 02 Jul 2014 12:12:26 +0200 |
wenzelm |
check 'case' variable bindings as for 'fix', which means internal names are rejected as usual;
|
changeset |
files
|
| Wed, 02 Jul 2014 08:03:50 +0200 |
haftmann |
optional exit hook for theory-like targets
|
changeset |
files
|
| Wed, 02 Jul 2014 08:03:49 +0200 |
haftmann |
restore exactly named target, prevent non-named targets to participate in the ad-hoc switch game
|
changeset |
files
|
| Wed, 02 Jul 2014 08:03:48 +0200 |
haftmann |
centralized (ad-hoc) switching of targets in named_target.ML
|
changeset |
files
|
| Tue, 01 Jul 2014 21:57:08 -0700 |
huffman |
add lemmas: polynomial div/mod distribute over addition
|
changeset |
files
|
| Tue, 01 Jul 2014 23:02:25 +0200 |
blanchet |
reverted 9512b867259c -- appears to break 'metis'
|
changeset |
files
|
| Tue, 01 Jul 2014 21:07:02 +0200 |
wenzelm |
clarified "axiomatization" -- minor rewording of this delicate concept;
|
changeset |
files
|
| Tue, 01 Jul 2014 20:47:25 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 01 Jul 2014 20:43:51 +0200 |
wenzelm |
more on ML options;
|
changeset |
files
|
| Tue, 01 Jul 2014 17:59:56 +0200 |
wenzelm |
redundant error position, to ensure the message is attached somewhere, despite the distortion of positions due to glued tokens;
|
changeset |
files
|
| Tue, 01 Jul 2014 17:16:11 +0200 |
immler |
overdue NEWS concerning c4daa97ac57a
|
changeset |
files
|
| Tue, 01 Jul 2014 16:09:51 +0100 |
paulson |
Merge
|
changeset |
files
|
| Tue, 01 Jul 2014 16:08:31 +0100 |
paulson |
for new release
|
changeset |
files
|
| Tue, 01 Jul 2014 17:06:54 +0200 |
desharna |
merge
|
changeset |
files
|
| Tue, 01 Jul 2014 17:01:48 +0200 |
desharna |
document property 'rel_induct'
|
changeset |
files
|
| Tue, 01 Jul 2014 17:01:28 +0200 |
desharna |
generate 'rel_induct' theorem for datatypes
|
changeset |
files
|
| Tue, 01 Jul 2014 16:49:25 +0200 |
blanchet |
fixed soundness bug in monotonicity-based type encodings -- the helper facts must be considered too
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
whitespace tuning
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
robustness in the face of ill-typed "unchecked" terms (e.g. case expressions)
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
use context instead of theory
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
fine-tuned methods
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
tuned message
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
updated docs
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
changed default MaSh engine
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
removed needless code
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
speed up MaSh a bit
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
mix NB and kNN
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
tuned (reordered) code
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
clean up MaSh export a bit
|
changeset |
files
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
clean up MaSh evaluation driver
|
changeset |
files
|
| Tue, 01 Jul 2014 16:26:14 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 01 Jul 2014 15:19:43 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 01 Jul 2014 15:19:05 +0200 |
wenzelm |
clarified quasi-generic PIDE;
|
changeset |
files
|
| Tue, 01 Jul 2014 14:52:08 +0200 |
wenzelm |
misc updates for release;
|
changeset |
files
|
| Tue, 01 Jul 2014 14:05:05 +0200 |
wenzelm |
more release notes;
|
changeset |
files
|
| Tue, 01 Jul 2014 15:57:07 +0200 |
hoelzl |
Library/Tree: bst is preferred to be a function
|
changeset |
files
|
| Tue, 01 Jul 2014 15:25:27 +0200 |
hoelzl |
Library/Tree: use datatype_new, bst is an inductive predicate
|
changeset |
files
|
| Mon, 30 Jun 2014 15:45:25 +0200 |
hoelzl |
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
|
changeset |
files
|
| Mon, 30 Jun 2014 15:45:21 +0200 |
hoelzl |
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
|
changeset |
files
|
| Mon, 30 Jun 2014 15:45:03 +0200 |
hoelzl |
some lemmas about the indicator function; removed lemma sums_def2
|
changeset |
files
|
| Tue, 01 Jul 2014 11:06:31 +0200 |
traytel |
generate type correct terms in uncheck phase
|
changeset |
files
|
| Mon, 30 Jun 2014 15:23:00 +0200 |
wenzelm |
updated to sumatra_pdf-2.5.2;
|
changeset |
files
|
| Mon, 30 Jun 2014 10:53:37 +0200 |
wenzelm |
ProofGeneral-4.2-2 is optional component (including the traditional helper scripts);
|
changeset |
files
|
| Mon, 30 Jun 2014 10:34:28 +0200 |
wenzelm |
removed obsolete Isar system commands -- raw ML console is normally used for system tinkering;
|
changeset |
files
|
| Mon, 30 Jun 2014 10:10:32 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Mon, 30 Jun 2014 10:00:16 +0200 |
wenzelm |
updated README;
|
changeset |
files
|
| Mon, 30 Jun 2014 09:43:44 +0200 |
wenzelm |
"isabelle tty" is superseded by "isabelle console";
|
changeset |
files
|
| Mon, 30 Jun 2014 09:31:32 +0200 |
wenzelm |
tuned description: fit into 80 chars terminal;
|
changeset |
files
|
| Mon, 30 Jun 2014 08:00:36 +0200 |
haftmann |
qualified String.explode and String.implode
|
changeset |
files
|
| Sun, 29 Jun 2014 21:07:53 +0200 |
blanchet |
removed non-existing MaSh component from list
|
changeset |
files
|
| Sun, 29 Jun 2014 18:02:18 +0200 |
haftmann |
modernized diagnostic options
|
changeset |
files
|
| Sun, 29 Jun 2014 18:30:24 +0200 |
blanchet |
use SMT2
|
changeset |
files
|
| Sun, 29 Jun 2014 18:28:27 +0200 |
blanchet |
compile
|
changeset |
files
|
| Sun, 29 Jun 2014 18:28:27 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Sun, 29 Jun 2014 18:28:27 +0200 |
blanchet |
killed Python version of MaSh, now that the SML version works adequately
|
changeset |
files
|
| Sat, 28 Jun 2014 22:13:23 +0200 |
haftmann |
tracing facilities for the code generator preprocessor
|
changeset |
files
|
| Sat, 28 Jun 2014 22:13:21 +0200 |
haftmann |
tuned interface
|
changeset |
files
|
| Sat, 28 Jun 2014 22:13:20 +0200 |
haftmann |
corrected handled exception
|
changeset |
files
|
| Sat, 28 Jun 2014 21:09:17 +0200 |
haftmann |
proper trading of variables;
|
changeset |
files
|
| Sat, 28 Jun 2014 21:09:15 +0200 |
haftmann |
modernized
|
changeset |
files
|
| Sat, 28 Jun 2014 18:02:33 +0200 |
wenzelm |
jedit_completion_immediate is enabled by default: let all users participate in slightly more ambitious symbol insertion;
|
changeset |
files
|
| Sat, 28 Jun 2014 17:54:34 +0200 |
wenzelm |
removed slightly odd fall-back on complete-word (NB: connection to default menu action is unclear);
|
changeset |
files
|
| Sat, 28 Jun 2014 15:50:48 +0200 |
wenzelm |
updated NEWS -- removed material that is already in the manual;
|
changeset |
files
|
| Sat, 28 Jun 2014 15:35:30 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 28 Jun 2014 15:34:43 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Sat, 28 Jun 2014 11:19:58 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Sat, 28 Jun 2014 11:44:22 +0200 |
haftmann |
CONTRIBUTORS
|
changeset |
files
|
| Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
changeset |
files
|
| Fri, 27 Jun 2014 22:08:55 +0200 |
wenzelm |
more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
|
changeset |
files
|
| Fri, 27 Jun 2014 19:38:32 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 27 Jun 2014 16:04:56 +0200 |
wenzelm |
command 'print_term_bindings' supersedes 'print_binds';
|
changeset |
files
|
| Fri, 27 Jun 2014 15:41:26 +0200 |
wenzelm |
Proof General legacy;
|
changeset |
files
|
| Fri, 27 Jun 2014 15:30:57 +0200 |
wenzelm |
removed obsolete "isabelle unsymbolize";
|
changeset |
files
|
| Fri, 27 Jun 2014 15:24:56 +0200 |
wenzelm |
minor renovation of slightly odd and old README;
|
changeset |
files
|
| Fri, 27 Jun 2014 11:30:42 +0200 |
wenzelm |
sane environment defaults for Mac OS X, based on former App1/script -- e.g. relevant for MacTeX PATH;
|
changeset |
files
|
| Fri, 27 Jun 2014 19:21:58 +0200 |
blanchet |
tweaking
|
changeset |
files
|
| Fri, 27 Jun 2014 19:17:16 +0200 |
blanchet |
correctly take weights into consideration
|
changeset |
files
|
| Fri, 27 Jun 2014 18:27:37 +0200 |
blanchet |
tuned whitespace and parentheses
|
changeset |
files
|
| Fri, 27 Jun 2014 17:18:30 +0200 |
blanchet |
use right theory name for theorems in evaluation driver
|
changeset |
files
|
| Fri, 27 Jun 2014 17:05:22 +0200 |
blanchet |
killed dead code
|
changeset |
files
|
| Fri, 27 Jun 2014 16:52:50 +0200 |
blanchet |
reintroduced 'extra features' + only print message in verbose mode
|
changeset |
files
|
| Fri, 27 Jun 2014 14:20:50 +0200 |
blanchet |
got rid of hard-coded weights, now that we have TFIDF
|
changeset |
files
|
| Fri, 27 Jun 2014 12:06:22 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 27 Jun 2014 11:56:28 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 27 Jun 2014 11:38:15 +0200 |
blanchet |
reintroduced 'extra features' but with lower weight than before (to account for tfidf)
|
changeset |
files
|
| Fri, 27 Jun 2014 10:49:52 +0200 |
blanchet |
resolution modulo double negation
|
changeset |
files
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
compile
|
changeset |
files
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
merged two small theory files
|
changeset |
files
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
tuned variable names
|
changeset |
files
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
whitespace tuning
|
changeset |
files
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
repaired BNF 'size' generation tactic for datatypes mixng old- and new-style datatypes on the right-hand side
|
changeset |
files
|
| Fri, 27 Jun 2014 00:21:11 +0100 |
paulson |
tiny refinements
|
changeset |
files
|
| Thu, 26 Jun 2014 22:50:02 +0200 |
wenzelm |
suppress documentation "how_to_prove_it" for now, notably for release;
|
changeset |
files
|
| Thu, 26 Jun 2014 22:18:09 +0200 |
wenzelm |
updated to jdk-7u60 -- back to stable Java 7 for Isabelle2014 release;
|
changeset |
files
|
| Thu, 26 Jun 2014 22:01:40 +0200 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Thu, 26 Jun 2014 21:25:41 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 26 Jun 2014 19:46:07 +0200 |
wenzelm |
updated cygwin on server;
|
changeset |
files
|
| Thu, 26 Jun 2014 20:49:34 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 26 Jun 2014 20:32:31 +0200 |
blanchet |
reintroduced MaSh hints, this time as persistent creatures
|
changeset |
files
|
| Thu, 26 Jun 2014 19:40:58 +0200 |
blanchet |
always expand all paths
|
changeset |
files
|
| Thu, 26 Jun 2014 19:10:34 +0200 |
blanchet |
tuned output
|
changeset |
files
|
| Thu, 26 Jun 2014 18:57:20 +0200 |
blanchet |
tuned output
|
changeset |
files
|
| Thu, 26 Jun 2014 16:41:43 +0200 |
blanchet |
right array indexing
|
changeset |
files
|
| Thu, 26 Jun 2014 16:41:30 +0200 |
blanchet |
incremental learning when learing several facts
|
changeset |
files
|
| Thu, 26 Jun 2014 16:41:30 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 26 Jun 2014 16:41:30 +0200 |
blanchet |
more incremental learning of single fact
|
changeset |
files
|
| Thu, 26 Jun 2014 16:41:30 +0200 |
blanchet |
avoid needless (trivial) reordering on load
|
changeset |
files
|
| Thu, 26 Jun 2014 16:41:30 +0200 |
blanchet |
recompute learning data at learning time, not query time
|
changeset |
files
|
| Thu, 26 Jun 2014 16:41:30 +0200 |
blanchet |
imported patch killed_num_known_facts0
|
changeset |
files
|
| Thu, 26 Jun 2014 13:36:25 +0200 |
blanchet |
refactoring
|
changeset |
files
|
| Thu, 26 Jun 2014 13:36:22 +0200 |
blanchet |
renamed experimental learning engines
|
changeset |
files
|
| Thu, 26 Jun 2014 13:36:13 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 26 Jun 2014 13:36:06 +0200 |
blanchet |
refactoring
|
changeset |
files
|
| Thu, 26 Jun 2014 13:36:00 +0200 |
blanchet |
removed experimental machine learning engine
|
changeset |
files
|
| Thu, 26 Jun 2014 13:35:56 +0200 |
blanchet |
store string-to-index tables in memory
|
changeset |
files
|
| Thu, 26 Jun 2014 13:35:52 +0200 |
blanchet |
disable 'extra' feature tainting for now
|
changeset |
files
|
| Thu, 26 Jun 2014 13:35:46 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 26 Jun 2014 13:35:39 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 26 Jun 2014 13:35:36 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 26 Jun 2014 13:35:30 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 26 Jun 2014 13:35:21 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 26 Jun 2014 13:35:17 +0200 |
blanchet |
honor visible in SML naive Bayes
|
changeset |
files
|
| Thu, 26 Jun 2014 13:35:12 +0200 |
blanchet |
honor visibility in SML k-NN
|
changeset |
files
|
| Thu, 26 Jun 2014 13:35:07 +0200 |
blanchet |
got rid of a few experimental options
|
changeset |
files
|
| Thu, 26 Jun 2014 13:35:00 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 26 Jun 2014 13:34:57 +0200 |
blanchet |
killed dead code
|
changeset |
files
|
| Thu, 26 Jun 2014 13:34:50 +0200 |
blanchet |
avoid subscripting array with ~1
|
changeset |
files
|
| Thu, 26 Jun 2014 13:34:39 +0200 |
blanchet |
killed dead data
|
changeset |
files
|
| Thu, 26 Jun 2014 13:34:28 +0200 |
blanchet |
new version of adaptive k-NN with TFIDF
|
changeset |
files
|
| Thu, 26 Jun 2014 13:33:50 +0200 |
blanchet |
refactoring
|
changeset |
files
|
| Thu, 26 Jun 2014 13:33:27 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 26 Jun 2014 13:33:21 +0200 |
blanchet |
refactoring
|
changeset |
files
|
| Thu, 26 Jun 2014 13:33:08 +0200 |
blanchet |
adaptive k-NN
|
changeset |
files
|
| Thu, 26 Jun 2014 13:33:02 +0200 |
blanchet |
avoid parallelism, since it confuses the global state and leads to cheating (with 'sml_xxx' engines)
|
changeset |
files
|
| Thu, 26 Jun 2014 13:32:56 +0200 |
blanchet |
generate right dependencies in MaSh driver
|
changeset |
files
|
| Mon, 23 Jun 2014 12:54:48 +0200 |
wenzelm |
more on "Futures";
|
changeset |
files
|
| Mon, 23 Jun 2014 12:20:20 +0200 |
wenzelm |
more on "Futures";
|
changeset |
files
|