| Tue, 23 May 2023 18:46:15 +0200 |
wenzelm |
tuned signature: more position information;
|
file |
diff |
annotate
|
| Tue, 18 Apr 2023 22:24:48 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Tue, 19 Oct 2021 14:58:22 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Tue, 28 Sep 2021 22:12:52 +0200 |
wenzelm |
clarified antiquotations;
|
file |
diff |
annotate
|
| Fri, 10 Sep 2021 14:59:19 +0200 |
wenzelm |
clarified signature: more scalable operations;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2021 12:33:14 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 26 Aug 2021 14:45:19 +0200 |
wenzelm |
more scalable data structure (but: rarely used with > 5 arguments);
|
file |
diff |
annotate
|
| Mon, 12 Oct 2020 07:25:38 +0000 |
haftmann |
consolidated names and operations
|
file |
diff |
annotate
|
| Fri, 14 Aug 2020 14:40:24 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 02 Dec 2019 15:04:38 +0100 |
wenzelm |
proper spec_rule name via naming/binding/Morphism.binding;
|
file |
diff |
annotate
|
| Fri, 29 Nov 2019 20:57:04 +0100 |
wenzelm |
more informative spec rules: optional name;
|
file |
diff |
annotate
|
| Fri, 09 Aug 2019 17:14:49 +0200 |
wenzelm |
formal position for PThm nodes;
|
file |
diff |
annotate
|
| Tue, 26 Mar 2019 22:13:36 +0100 |
wenzelm |
more informative Spec_Rules.Equational, notably primrec argument types;
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Fri, 23 Feb 2018 19:25:37 +0100 |
wenzelm |
added HOLogic.mk_obj_eq convenience and eliminated some clones;
|
file |
diff |
annotate
|
| Thu, 22 Feb 2018 14:28:05 +0100 |
wenzelm |
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
|
| Fri, 23 Dec 2016 00:13:30 +0100 |
blanchet |
generalized generation of coinduction goal (towards nonuniform codatatypes)
|
file |
diff |
annotate
|
| Thu, 22 Dec 2016 19:14:58 +0100 |
blanchet |
export ML functions (towards nonuniform codatatypes) + signature tuning
|
file |
diff |
annotate
|
| Wed, 21 Dec 2016 12:49:15 +0100 |
blanchet |
generalized ML function (towards nonuniform datatypes)
|
file |
diff |
annotate
|
| Wed, 21 Dec 2016 11:45:16 +0100 |
blanchet |
generalized ML function (towards nonuniform datatypes)
|
file |
diff |
annotate
|
| Wed, 21 Dec 2016 11:14:37 +0100 |
blanchet |
renamed confusing variable names
|
file |
diff |
annotate
|
| Tue, 20 Dec 2016 16:17:13 +0100 |
blanchet |
generalized code (towards nonuniform datatypes)
|
file |
diff |
annotate
|
| Fri, 16 Dec 2016 22:54:14 +0100 |
blanchet |
refactored induction principle generation code, for reuse for nonuniform datatypes
|
file |
diff |
annotate
|
| Thu, 27 Oct 2016 14:14:58 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 27 Oct 2016 14:14:48 +0200 |
blanchet |
more uniform treatment of codatatype vs. datatype map and rel theorem generation (towards nonuniform codatatypes)
|
file |
diff |
annotate
|
| Wed, 26 Oct 2016 22:40:28 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 06 Oct 2016 13:33:26 +0200 |
traytel |
less aggressive unfolding in tactic
|
file |
diff |
annotate
|
| Tue, 13 Sep 2016 16:23:12 +0200 |
blanchet |
union associates to the left
|
file |
diff |
annotate
|
| Mon, 12 Sep 2016 23:17:55 +0200 |
blanchet |
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
|
file |
diff |
annotate
|
| Mon, 12 Sep 2016 16:51:55 +0200 |
blanchet |
avoid warning triggered by code generator
|
file |
diff |
annotate
|
| Mon, 12 Sep 2016 13:35:29 +0200 |
blanchet |
prove 'set' property backward
|
file |
diff |
annotate
|
| Sun, 11 Sep 2016 23:32:45 +0200 |
blanchet |
generalized code towards nonuniform (co)datatypes
|
file |
diff |
annotate
|
| Sun, 11 Sep 2016 15:37:09 +0200 |
blanchet |
strengthened tactics
|
file |
diff |
annotate
|
| Sun, 11 Sep 2016 13:35:27 +0200 |
blanchet |
derive relator properties forward
|
file |
diff |
annotate
|
| Sun, 11 Sep 2016 13:35:27 +0200 |
blanchet |
derive maps forward
|
file |
diff |
annotate
|
| Sun, 11 Sep 2016 13:35:27 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Sun, 11 Sep 2016 13:35:27 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 08 Sep 2016 10:35:08 +0200 |
blanchet |
made it easier to catch 'empty datatype' exception
|
file |
diff |
annotate
|
| Thu, 08 Sep 2016 10:16:39 +0200 |
blanchet |
export ML functions
|
file |
diff |
annotate
|
| Thu, 08 Sep 2016 10:16:37 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 07 Sep 2016 16:06:59 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 07 Sep 2016 13:53:16 +0200 |
blanchet |
exported ML functions + tuning
|
file |
diff |
annotate
|
| Wed, 07 Sep 2016 13:53:16 +0200 |
blanchet |
refactoring
|
file |
diff |
annotate
|
| Wed, 07 Sep 2016 13:53:16 +0200 |
blanchet |
refactoring
|
file |
diff |
annotate
|
| Wed, 07 Sep 2016 13:53:16 +0200 |
blanchet |
refactoring
|
file |
diff |
annotate
|
| Wed, 07 Sep 2016 13:53:16 +0200 |
blanchet |
tuned whitespace
|
file |
diff |
annotate
|
| Tue, 06 Sep 2016 15:23:01 +0200 |
blanchet |
export more ML functions
|
file |
diff |
annotate
|
| Tue, 06 Sep 2016 15:04:02 +0200 |
blanchet |
generalized ML signature
|
file |
diff |
annotate
|
| Tue, 06 Sep 2016 10:09:33 +0200 |
blanchet |
tuned ML signature
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 20:57:07 +0200 |
blanchet |
exported ML functions
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 18:40:29 +0200 |
blanchet |
export ML function + tuning
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 13:09:18 +0200 |
blanchet |
export more ML functions
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 11:35:42 +0200 |
blanchet |
export more ML functions
|
file |
diff |
annotate
|
| Sun, 14 Aug 2016 12:26:09 +0200 |
blanchet |
tuned ML
|
file |
diff |
annotate
|
| Tue, 26 Jul 2016 14:29:20 +0200 |
traytel |
honor sorts in (co)datatype declarations
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 21:28:46 +0200 |
haftmann |
explicit tagging of code equations de-baroquifies interface
|
file |
diff |
annotate
|
| Thu, 02 Jun 2016 16:49:44 +0200 |
wenzelm |
eliminated pointless alias (no warning for duplicates);
|
file |
diff |
annotate
|