| 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
|