Fri, 20 Jan 2012 09:28:53 +0100 |
bulwahn |
adding narrowing instance for sets
|
changeset |
files
|
Fri, 20 Jan 2012 09:28:52 +0100 |
bulwahn |
shortened definitions by adding some termify constants
|
changeset |
files
|
Fri, 20 Jan 2012 09:28:51 +0100 |
bulwahn |
tuned
|
changeset |
files
|
Fri, 20 Jan 2012 09:28:50 +0100 |
bulwahn |
adding check_all instance for sets; tuned
|
changeset |
files
|
Fri, 20 Jan 2012 08:24:51 +0100 |
nipkow |
tuned
|
changeset |
files
|
Fri, 20 Jan 2012 07:55:43 +0100 |
nipkow |
tuned
|
changeset |
files
|
Thu, 19 Jan 2012 21:37:12 +0100 |
blanchet |
minor edits in docs
|
changeset |
files
|
Thu, 19 Jan 2012 21:37:12 +0100 |
blanchet |
renamed "sound" option to "strict"
|
changeset |
files
|
Thu, 19 Jan 2012 21:37:12 +0100 |
blanchet |
updated Sledge docs some more
|
changeset |
files
|
Thu, 19 Jan 2012 21:37:12 +0100 |
blanchet |
more doc updates
|
changeset |
files
|
Thu, 19 Jan 2012 21:37:12 +0100 |
blanchet |
updated docs
|
changeset |
files
|
Thu, 19 Jan 2012 21:37:12 +0100 |
blanchet |
lower timeout for preplay, now that we have more preplay methods
|
changeset |
files
|
Thu, 19 Jan 2012 21:37:12 +0100 |
blanchet |
cleanly separate each Metis encoding
|
changeset |
files
|
Thu, 09 Feb 2012 19:34:23 +0100 |
wenzelm |
basic setup for equational reasoning;
|
changeset |
files
|
Tue, 07 Feb 2012 18:56:40 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Tue, 07 Feb 2012 18:51:22 +0100 |
wenzelm |
updated examples for syntax translations;
|
changeset |
files
|
Sun, 05 Feb 2012 21:00:38 +0100 |
wenzelm |
updated section on raw syntax;
|
changeset |
files
|
Sun, 05 Feb 2012 18:11:19 +0100 |
wenzelm |
updated section about syntax ambiguity;
|
changeset |
files
|
Sat, 04 Feb 2012 18:33:04 +0100 |
wenzelm |
updated/unified section on mixfix annotations;
|
changeset |
files
|
Sat, 04 Feb 2012 16:08:19 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Sat, 04 Feb 2012 15:56:49 +0100 |
wenzelm |
more on explicit notation;
|
changeset |
files
|
Sat, 04 Feb 2012 15:44:50 +0100 |
wenzelm |
more accurate Pure grammar;
|
changeset |
files
|
Sat, 04 Feb 2012 14:25:14 +0100 |
wenzelm |
more refs;
|
changeset |
files
|
Sat, 04 Feb 2012 14:20:39 +0100 |
wenzelm |
simplified mixfix (NB: infix is no longer required separately);
|
changeset |
files
|
Thu, 02 Feb 2012 21:21:41 +0100 |
wenzelm |
updated section on print modes;
|
changeset |
files
|
Thu, 02 Feb 2012 20:26:44 +0100 |
wenzelm |
misc tuning and reformatting;
|
changeset |
files
|
Thu, 02 Feb 2012 18:11:42 +0100 |
wenzelm |
clarified syntax section structure;
|
changeset |
files
|
Thu, 02 Feb 2012 17:52:16 +0100 |
wenzelm |
discontinued obscure history commands;
|
changeset |
files
|
Thu, 02 Feb 2012 16:38:15 +0100 |
wenzelm |
misc tuning and reformatting;
|
changeset |
files
|
Thu, 02 Feb 2012 16:07:25 +0100 |
wenzelm |
discontinued obscure history commands;
|
changeset |
files
|
Sun, 29 Jan 2012 22:12:25 +0100 |
wenzelm |
updated hint about asm_rl;
|
changeset |
files
|
Sun, 29 Jan 2012 22:00:10 +0100 |
wenzelm |
updated thin_tac;
|
changeset |
files
|
Sun, 29 Jan 2012 21:40:29 +0100 |
wenzelm |
updated distinct_subgoals_tac, flexflex_tac;
|
changeset |
files
|
Sun, 29 Jan 2012 21:26:09 +0100 |
wenzelm |
removed obscure material;
|
changeset |
files
|
Sun, 29 Jan 2012 21:04:39 +0100 |
wenzelm |
updated rotate_tac;
|
changeset |
files
|
Fri, 27 Jan 2012 21:56:29 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 27 Jan 2012 21:48:40 +0100 |
wenzelm |
updated citations;
|
changeset |
files
|
Fri, 27 Jan 2012 21:29:37 +0100 |
wenzelm |
updated subgoal_tac;
|
changeset |
files
|
Thu, 26 Jan 2012 22:21:33 +0100 |
wenzelm |
tuned sectioning;
|
changeset |
files
|
Thu, 26 Jan 2012 22:16:45 +0100 |
wenzelm |
updated "Control and search tacticals" (moved from ref to implementation);
|
changeset |
files
|
Thu, 26 Jan 2012 21:25:18 +0100 |
wenzelm |
obsolete -- covered in implementation manual;
|
changeset |
files
|
Thu, 26 Jan 2012 21:16:11 +0100 |
wenzelm |
moved HEADGOAL;
|
changeset |
files
|
Thu, 26 Jan 2012 15:29:11 +0100 |
wenzelm |
removed some obscure material;
|
changeset |
files
|
Thu, 26 Jan 2012 15:28:17 +0100 |
wenzelm |
added SELECT_GOAL;
|
changeset |
files
|
Thu, 26 Jan 2012 15:04:35 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Wed, 25 Jan 2012 22:01:15 +0100 |
wenzelm |
updated "subgoal quantifiers";
|
changeset |
files
|
Wed, 25 Jan 2012 21:14:00 +0100 |
wenzelm |
tuned ML infixes;
|
changeset |
files
|
Wed, 25 Jan 2012 21:10:54 +0100 |
wenzelm |
document antiquotations for ML infix operators;
|
changeset |
files
|
Wed, 25 Jan 2012 20:26:05 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Wed, 25 Jan 2012 19:04:38 +0100 |
wenzelm |
updated repetition tacticals;
|
changeset |
files
|
Wed, 25 Jan 2012 18:18:59 +0100 |
wenzelm |
updated THEN, ORELSE, APPEND, and derivatives;
|
changeset |
files
|
Wed, 25 Jan 2012 16:16:20 +0100 |
wenzelm |
removed obscure/outdated material;
|
changeset |
files
|
Wed, 25 Jan 2012 15:39:08 +0100 |
wenzelm |
updated RSN, RL, RLN, MRS;
|
changeset |
files
|
Wed, 25 Jan 2012 14:13:59 +0100 |
wenzelm |
removed obscure/outdated material;
|
changeset |
files
|
Wed, 25 Jan 2012 13:31:56 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Wed, 25 Jan 2012 13:24:57 +0100 |
wenzelm |
more on Logic.all/mk_implies etc.;
|
changeset |
files
|
Thu, 19 Jan 2012 16:16:13 +0100 |
wenzelm |
reduce AFP test by many hours;
|
changeset |
files
|
Thu, 19 Jan 2012 09:51:42 +0100 |
nipkow |
added termination of narrowing
|
changeset |
files
|
Wed, 18 Jan 2012 22:06:31 +0100 |
wenzelm |
really need 64bit here;
|
changeset |
files
|
Wed, 18 Jan 2012 13:04:58 +0100 |
nipkow |
Added termination proof for widening
|
changeset |
files
|