| Mon, 02 Dec 2019 16:28:23 +0100 |
wenzelm |
clarified name: avoid clashes;
|
file |
diff |
annotate
|
| Mon, 02 Dec 2019 15:04:38 +0100 |
wenzelm |
proper spec_rule name via naming/binding/Morphism.binding;
|
file |
diff |
annotate
|
| Mon, 02 Dec 2019 13:34:02 +0100 |
wenzelm |
more informative spec rules;
|
file |
diff |
annotate
|
| Fri, 29 Nov 2019 20:57:04 +0100 |
wenzelm |
more informative spec rules: optional name;
|
file |
diff |
annotate
|
| Thu, 19 Sep 2019 15:09:12 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 18 Sep 2019 20:10:15 +0200 |
wenzelm |
more robust declaration of resulting statement text, instead of somewhat accidental (Variable.maybe_bind_term result_binds in generic_goal);
|
file |
diff |
annotate
|
| Mon, 03 Jun 2019 15:40:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 26 Mar 2019 22:13:36 +0100 |
wenzelm |
more informative Spec_Rules.Equational, notably primrec argument types;
|
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
|
| Mon, 03 Jul 2017 13:51:55 +0200 |
wenzelm |
added command 'alias' and 'type_alias';
|
file |
diff |
annotate
|
| Tue, 05 Jul 2016 20:51:02 +0200 |
wenzelm |
PIDE reports of implicit variable scope;
|
file |
diff |
annotate
|
| Tue, 05 Jul 2016 14:20:27 +0200 |
wenzelm |
PIDE reports of implicit variable scope;
|
file |
diff |
annotate
|
| Tue, 05 Jul 2016 10:32:25 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 23 Jun 2016 11:01:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2016 12:02:38 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 21:28:46 +0200 |
haftmann |
explicit tagging of code equations de-baroquifies interface
|
file |
diff |
annotate
|
| Mon, 30 May 2016 14:15:44 +0200 |
wenzelm |
allow 'for' fixes for multi_specs;
|
file |
diff |
annotate
|
| Mon, 30 May 2016 11:44:41 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Sun, 29 May 2016 15:40:25 +0200 |
wenzelm |
clarified check_open_spec / read_open_spec;
|
file |
diff |
annotate
|
| Sat, 28 May 2016 23:55:41 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 28 May 2016 21:38:58 +0200 |
wenzelm |
clarified 'axiomatization';
|
file |
diff |
annotate
|
| Sat, 14 May 2016 22:00:44 +0200 |
wenzelm |
re-enable fact index for 'obtains' assumption (amending 5c8e6a751adc);
|
file |
diff |
annotate
|
| Sat, 14 May 2016 19:49:10 +0200 |
wenzelm |
toplevel theorem statements support 'if'/'for' eigen-context;
|
file |
diff |
annotate
|
| Fri, 29 Apr 2016 01:21:44 +0200 |
wenzelm |
re-tuned c9605a284fba, which impacts performance significantly (for unclear reasons) -- make AFP/Collections build again;
|
file |
diff |
annotate
|
| Thu, 28 Apr 2016 11:31:36 +0200 |
wenzelm |
clarified order: params/prems/concl interchangeable with !!/==> proposition;
|
file |
diff |
annotate
|
| Thu, 28 Apr 2016 09:43:11 +0200 |
wenzelm |
support 'assumes' in specifications, e.g. 'definition', 'inductive';
|
file |
diff |
annotate
|
| Wed, 27 Apr 2016 10:03:35 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 16:54:48 +0200 |
wenzelm |
clarified def binding position: reset for implicit/derived binding, keep for explicit binding;
|
file |
diff |
annotate
|
| Sun, 24 Apr 2016 20:37:24 +0200 |
wenzelm |
within a proof body context, undeclared frees are like global constants;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2016 20:24:19 +0200 |
wenzelm |
prefer internal attribute source;
|
file |
diff |
annotate
|