| Fri, 10 Sep 2021 14:59:19 +0200 |
wenzelm |
clarified signature: more scalable operations;
|
file |
diff |
annotate
|
| Mon, 06 Sep 2021 12:23:06 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 04 Aug 2021 19:41:59 +0200 |
wenzelm |
clarified export of formal entities: name space info is always present, but content depends on option "export_theory";
|
file |
diff |
annotate
|
| Fri, 21 May 2021 12:29:29 +0200 |
wenzelm |
clarified modules;
|
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
|
| Fri, 06 Dec 2019 17:05:52 +0100 |
wenzelm |
suppress record types: not working properly;
|
file |
diff |
annotate
|
| Fri, 06 Dec 2019 15:53:09 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 06 Dec 2019 15:44:55 +0100 |
wenzelm |
export datatypes;
|
file |
diff |
annotate
|
| Fri, 06 Dec 2019 11:43:29 +0100 |
wenzelm |
clarified modules;
|
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
|
| 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
|
| Sun, 02 Jul 2017 20:13:38 +0200 |
haftmann |
proper concept of code declaration wrt. atomicity and Isar declarations
|
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, 12 Sep 2016 16:51:55 +0200 |
blanchet |
avoid warning triggered by code generator
|
file |
diff |
annotate
|
| Fri, 17 Jun 2016 21:25:59 +0200 |
blanchet |
avoid runtime warning with discriminators due to 'Code.del_eqn'
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 21:28:46 +0200 |
haftmann |
explicit tagging of code equations de-baroquifies interface
|
file |
diff |
annotate
|
| Sun, 29 May 2016 15:40:25 +0200 |
wenzelm |
clarified check_open_spec / read_open_spec;
|
file |
diff |
annotate
|
| Thu, 28 Apr 2016 09:43:11 +0200 |
wenzelm |
support 'assumes' in specifications, e.g. 'definition', 'inductive';
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 11:54:34 +0100 |
blanchet |
allow predicator instead of map function in 'primrec'
|
file |
diff |
annotate
|
| Mon, 15 Feb 2016 18:27:17 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 15 Feb 2016 12:48:10 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 01 Dec 2015 13:07:40 +0100 |
blanchet |
tuned whitespace
|
file |
diff |
annotate
|
| Mon, 02 Nov 2015 21:49:49 +0100 |
blanchet |
allow selectors and discriminators with same name as type
|
file |
diff |
annotate
|