| Wed, 02 Oct 2024 22:08:52 +0200 |
wenzelm |
provide 'open_bundle' command;
|
file |
diff |
annotate
|
| Thu, 08 Aug 2024 16:03:34 +0200 |
wenzelm |
tuned: more antiquotations;
|
file |
diff |
annotate
|
| Sun, 04 Aug 2024 17:39:47 +0200 |
wenzelm |
tuned: more explicit dest_Const_name and dest_Const_type;
|
file |
diff |
annotate
|
| Sun, 04 Aug 2024 13:24:54 +0200 |
wenzelm |
tuned: more explicit dest_Type_name and dest_Type_args;
|
file |
diff |
annotate
|
| Sun, 24 Sep 2023 15:55:42 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 23 May 2023 18:46:15 +0200 |
wenzelm |
tuned signature: more position information;
|
file |
diff |
annotate
|
| Sat, 20 May 2023 22:41:37 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 04 Jun 2022 15:43:34 +0200 |
desharna |
introduced predicate reflp_on and redefined reflp to be an abbreviation
|
file |
diff |
annotate
|
| Tue, 19 Oct 2021 14:58:22 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2021 12:33:14 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2021 18:57:33 +0200 |
wenzelm |
more scalable data structure (but: rarely used many arguments);
|
file |
diff |
annotate
|
| Mon, 16 Aug 2021 11:49:39 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 12 Oct 2020 07:25:38 +0000 |
haftmann |
avoid _cmd suffix where no Isar command is involved
|
file |
diff |
annotate
|
| Tue, 06 Aug 2019 17:26:40 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 04 Jun 2019 17:04:18 +0200 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Tue, 04 Jun 2019 16:47:05 +0200 |
wenzelm |
proper context;
|
file |
diff |
annotate
|
| Tue, 04 Jun 2019 15:14:56 +0200 |
wenzelm |
misc tuning and clarification, notably wrt. flow of context;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Tue, 27 Nov 2018 21:07:39 +0100 |
wenzelm |
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
|
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
|
| Sun, 02 Jul 2017 20:13:38 +0200 |
haftmann |
proper concept of code declaration wrt. atomicity and Isar declarations
|
file |
diff |
annotate
|
| Tue, 05 Jul 2016 14:20:27 +0200 |
wenzelm |
PIDE reports of implicit variable scope;
|
file |
diff |
annotate
|
| Thu, 23 Jun 2016 11:01:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 29 May 2016 15:40:25 +0200 |
wenzelm |
clarified check_open_spec / read_open_spec;
|
file |
diff |
annotate
|
| Fri, 27 May 2016 20:23:55 +0200 |
wenzelm |
tuned proofs, to allow unfold_abs_def;
|
file |
diff |
annotate
|
| Mon, 23 May 2016 20:45:10 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 28 Apr 2016 09:43:11 +0200 |
wenzelm |
support 'assumes' in specifications, e.g. 'definition', 'inductive';
|
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
|
| Sun, 17 Apr 2016 20:11:02 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|