| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Sat, 16 Oct 2021 20:32:25 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Sat, 16 Oct 2021 20:21:13 +0200 |
wenzelm |
more accurate treatment of context;
|
file |
diff |
annotate
|
| Fri, 15 Oct 2021 19:25:31 +0200 |
wenzelm |
discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
|
file |
diff |
annotate
|
| Thu, 14 Oct 2021 16:03:20 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 10 Sep 2021 14:59:19 +0200 |
wenzelm |
clarified signature: more scalable operations;
|
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
|
| 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
|
| 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
|
| Sun, 02 Jul 2017 20:13:38 +0200 |
haftmann |
proper concept of code declaration wrt. atomicity and Isar declarations
|
file |
diff |
annotate
|
| Tue, 13 Dec 2016 11:51:42 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 21:28:46 +0200 |
haftmann |
explicit tagging of code equations de-baroquifies interface
|
file |
diff |
annotate
|
| Tue, 05 Jan 2016 13:48:51 +0100 |
wenzelm |
updated headers;
|
file |
diff |
annotate
|
| Wed, 09 Dec 2015 16:36:26 +0100 |
wenzelm |
clarified type Token.src: plain token list, with usual implicit value assignment;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2015 22:31:21 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Sun, 06 Sep 2015 22:14:51 +0200 |
haftmann |
prefer "uncurry" as canonical name for case distinction on products in combinatorial view
|
file |
diff |
annotate
|
| Fri, 28 Aug 2015 11:52:06 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 19:25:08 +0200 |
wenzelm |
added Thm.chyps_of;
|
file |
diff |
annotate
|
| Tue, 28 Jul 2015 21:47:03 +0200 |
wenzelm |
more explicit context;
|
file |
diff |
annotate
|
| Sat, 25 Jul 2015 23:41:53 +0200 |
wenzelm |
updated to infer_instantiate;
|
file |
diff |
annotate
|
| Fri, 24 Jul 2015 22:16:39 +0200 |
wenzelm |
proper context;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:47:08 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Thu, 09 Jul 2015 15:20:54 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Sun, 05 Jul 2015 15:02:30 +0200 |
wenzelm |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
file |
diff |
annotate
|
| Fri, 19 Jun 2015 20:43:34 +0200 |
wenzelm |
removed dead code;
|
file |
diff |
annotate
|
| Fri, 19 Jun 2015 20:14:50 +0200 |
wenzelm |
discontinued unused 'defer_recdef';
|
file |
diff |
annotate
|
| Fri, 19 Jun 2015 19:45:01 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 19 Jun 2015 19:29:57 +0200 |
wenzelm |
removed dead code;
|
file |
diff |
annotate
|
| Fri, 19 Jun 2015 19:13:15 +0200 |
wenzelm |
moved sources;
|
file |
diff |
annotate
|