| Sun, 31 Dec 2023 22:04:41 +0100 |
wenzelm |
minor performance tuning: proper Same.operation;
|
file |
diff |
annotate
|
| Sun, 10 Dec 2023 13:39:40 +0100 |
wenzelm |
more general Logic.incr_indexes_operation;
|
file |
diff |
annotate
|
| Tue, 06 Jun 2023 21:02:37 +0200 |
wenzelm |
proper trim_context;
|
file |
diff |
annotate
|
| Tue, 06 Jun 2023 15:29:43 +0200 |
wenzelm |
proper exception positions;
|
file |
diff |
annotate
|
| Tue, 23 May 2023 18:46:15 +0200 |
wenzelm |
tuned signature: more position information;
|
file |
diff |
annotate
|
| Tue, 16 May 2023 19:52:50 +0200 |
wenzelm |
tuned: avoid duplication;
|
file |
diff |
annotate
|
| Mon, 15 May 2023 19:40:01 +0200 |
wenzelm |
more accurate Thm.trim_context / Thm.transfer;
|
file |
diff |
annotate
|
| Mon, 15 May 2023 15:14:19 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Mon, 15 May 2023 15:04:37 +0200 |
wenzelm |
clarified signature: avoid convoluted operations;
|
file |
diff |
annotate
|
| Tue, 02 May 2023 08:39:48 +0000 |
haftmann |
stripped unused functionality
|
file |
diff |
annotate
|
| Fri, 24 Mar 2023 18:30:17 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sat, 02 Apr 2022 17:03:35 +0000 |
haftmann |
pass constructor arity as part of case certficiate
|
file |
diff |
annotate
|
| Sun, 27 Mar 2022 19:27:52 +0000 |
haftmann |
prefer build combinator
|
file |
diff |
annotate
|
| Tue, 11 Jan 2022 06:47:47 +0000 |
haftmann |
more correct transfer
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Fri, 10 Sep 2021 14:59:19 +0200 |
wenzelm |
clarified signature: more scalable operations;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 22:17:15 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 12 Jul 2021 11:41:02 +0000 |
haftmann |
proper local context
|
file |
diff |
annotate
|
| Fri, 17 Jul 2020 19:10:24 +0200 |
wenzelm |
clarified -- avoid non-standard extend/merge;
|
file |
diff |
annotate
|
| Fri, 09 Aug 2019 17:14:49 +0200 |
wenzelm |
formal position for PThm nodes;
|
file |
diff |
annotate
|
| Sun, 23 Jun 2019 13:42:16 +0000 |
haftmann |
proper quasi-total merge
|
file |
diff |
annotate
|
| Fri, 17 Aug 2018 11:26:34 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sun, 18 Feb 2018 15:05:21 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 17 Feb 2018 18:42:26 +0100 |
wenzelm |
trim context of persistent data;
|
file |
diff |
annotate
|
| Sun, 28 Jan 2018 19:28:52 +0100 |
wenzelm |
clarified take/drop/chop prefix/suffix;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 18:59:33 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Wed, 08 Nov 2017 15:31:14 +0100 |
Lars Hupel |
strip some trailing spaces to force Pure rebuild after ce6454669360
|
file |
diff |
annotate
|
| Fri, 04 Aug 2017 08:12:37 +0200 |
haftmann |
compactified output
|
file |
diff |
annotate
|
| Thu, 03 Aug 2017 12:50:02 +0200 |
haftmann |
one single plugin for code type declarations avoids problems when bootstrapping new plugins over types which have been both declared concrete and abstract in their code historiy
|
file |
diff |
annotate
|
| Thu, 03 Aug 2017 12:50:01 +0200 |
haftmann |
uniform namespace handling for both concrete and abstract types, following 32e0da92c786
|
file |
diff |
annotate
|
| Thu, 03 Aug 2017 12:50:00 +0200 |
haftmann |
clarified
|
file |
diff |
annotate
|
| Thu, 03 Aug 2017 12:49:55 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Wed, 02 Aug 2017 20:33:39 +0200 |
haftmann |
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
|
file |
diff |
annotate
|
| Mon, 10 Jul 2017 19:48:58 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sun, 02 Jul 2017 20:13:38 +0200 |
haftmann |
proper concept of code declaration wrt. atomicity and Isar declarations
|
file |
diff |
annotate
|
| Sat, 24 Jun 2017 09:17:33 +0200 |
haftmann |
treat "undefined" constants internally as special form of case combinators
|
file |
diff |
annotate
|
| Thu, 22 Jun 2017 15:20:32 +0200 |
wenzelm |
more informative task_statistics;
|
file |
diff |
annotate
|
| Tue, 20 Jun 2017 13:07:49 +0200 |
haftmann |
deleting a code equation never leads to unimplemented function
|
file |
diff |
annotate
|
| Tue, 20 Jun 2017 08:01:56 +0200 |
haftmann |
do not print unimplemented functions
|
file |
diff |
annotate
|
| Tue, 20 Jun 2017 08:01:56 +0200 |
haftmann |
dropped void values
|
file |
diff |
annotate
|
| Tue, 20 Jun 2017 08:01:56 +0200 |
haftmann |
more uniform order of constructors
|
file |
diff |
annotate
|
| Tue, 20 Jun 2017 08:01:56 +0200 |
haftmann |
more consistent terminology
|
file |
diff |
annotate
|
| Tue, 20 Jun 2017 08:01:56 +0200 |
haftmann |
avoid name particle "the" where no selection is implied
|
file |
diff |
annotate
|
| Tue, 20 Jun 2017 08:01:56 +0200 |
haftmann |
more uniform ordering and naming of sections;
|
file |
diff |
annotate
|
| Tue, 20 Jun 2017 08:01:56 +0200 |
haftmann |
tuned internal signature
|
file |
diff |
annotate
|
| Tue, 20 Jun 2017 08:01:56 +0200 |
haftmann |
more explicit constructor name
|
file |
diff |
annotate
|
| Tue, 20 Jun 2017 08:01:56 +0200 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Mon, 05 Jun 2017 21:24:41 +0200 |
haftmann |
decomposed tuple
|
file |
diff |
annotate
|
| Mon, 05 Jun 2017 21:24:40 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 05 Jun 2017 21:24:39 +0200 |
haftmann |
clarified message
|
file |
diff |
annotate
|
| Sat, 29 Oct 2016 00:39:33 +0200 |
blanchet |
avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 22:22:05 +0200 |
haftmann |
clear distinction between different situations concerning strictness of code equations
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 21:28:46 +0200 |
haftmann |
tuned signature
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 21:28:46 +0200 |
haftmann |
more correct exception handling
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 21:28:46 +0200 |
haftmann |
explicit tagging of code equations de-baroquifies interface
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 21:28:45 +0200 |
haftmann |
dropped unused code
|
file |
diff |
annotate
|
| Mon, 09 May 2016 14:37:47 +0200 |
wenzelm |
clarified context, notably for internal use of Simplifier;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 19:25:08 +0200 |
wenzelm |
added Thm.chyps_of;
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 18:19:30 +0200 |
wenzelm |
prefer theory_id operations;
|
file |
diff |
annotate
|