| Sun, 28 Jan 2018 19:28:52 +0100 |
wenzelm |
clarified take/drop/chop prefix/suffix;
|
file |
diff |
annotate
|
| Thu, 11 Jan 2018 13:48:17 +0100 |
wenzelm |
uniform use of Standard ML op-infix -- eliminated warnings;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Sat, 05 Mar 2016 17:01:45 +0100 |
wenzelm |
tuned signature -- clarified modules;
|
file |
diff |
annotate
|
| Tue, 01 Dec 2015 22:24:37 +0100 |
blanchet |
removed needless ML function
|
file |
diff |
annotate
|
| Thu, 13 Aug 2015 11:05:19 +0200 |
wenzelm |
tuned signature, in accordance to sortBy in Scala;
|
file |
diff |
annotate
|
| Wed, 22 Apr 2015 20:14:43 +0200 |
wenzelm |
allow diagnostic proof commands with skip_proofs;
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 14:18:32 +0200 |
wenzelm |
explicit error for Toplevel.proof_of;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Sun, 11 Jan 2015 21:06:47 +0100 |
wenzelm |
tuned warnings: observe Context_Position.is_visible;
|
file |
diff |
annotate
|
| Mon, 03 Nov 2014 14:50:27 +0100 |
wenzelm |
eliminated unused int_only flag (see also c12484a27367);
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 11:36:41 +0100 |
wenzelm |
discontinued obsolete Output.urgent_message;
|
file |
diff |
annotate
|
| Wed, 29 Oct 2014 17:01:44 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
| Wed, 17 Sep 2014 08:23:53 +0200 |
blanchet |
support (finite values of) codatatypes in Quickcheck
|
file |
diff |
annotate
|
| Fri, 12 Sep 2014 11:16:47 +0200 |
blanchet |
fixed spellings
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 17:34:03 +0200 |
blanchet |
ported Refute to use new datatypes when possible
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
removed commented out parts
|
file |
diff |
annotate
|
| Sat, 09 Aug 2014 21:03:42 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 04 May 2014 19:08:29 +0200 |
blanchet |
tuned structure name
|
file |
diff |
annotate
|
| Sun, 04 May 2014 18:57:45 +0200 |
blanchet |
renamed 'dpll_p' to 'cdclite', to avoid confusion with the old 'dpll' and to reflect the idea that the new prover implements some ideas from CDCL not in DPLL -- this follows its author's, Sascha B.'s, wish
|
file |
diff |
annotate
|
| Sun, 04 May 2014 18:14:58 +0200 |
blanchet |
renamed 'xxx_size' to 'size_xxx' for old datatype package
|
file |
diff |
annotate
|
| Sun, 04 May 2014 16:17:53 +0200 |
boehmes |
removed obsolete internal SAT solvers
|
file |
diff |
annotate
|
| Thu, 01 May 2014 22:56:59 +0200 |
boehmes |
added internal proof-producing SAT solver
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 20:42:16 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 18:15:09 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 12:34:50 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 16:54:01 +0100 |
wenzelm |
prefer more robust Synchronized.var;
|
file |
diff |
annotate
|