| Wed, 11 Oct 2023 11:59:24 +0200 |
wenzelm |
proper Exn.capture / Isabelle_Thread.try_catch;
|
file |
diff |
annotate
|
| Fri, 26 May 2023 11:46:51 +0200 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Sat, 20 May 2023 21:48:41 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 20 May 2023 17:18:44 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 20 May 2023 12:04:41 +0200 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Fri, 19 May 2023 21:22:39 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 18 May 2023 23:50:59 +0200 |
wenzelm |
more careful reset/set_context for stored declarations;
|
file |
diff |
annotate
|
| Thu, 18 May 2023 17:21:29 +0200 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Tue, 16 May 2023 17:08:31 +0200 |
wenzelm |
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
|
file |
diff |
annotate
|
| Tue, 16 May 2023 15:15:56 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 16 May 2023 14:30:32 +0200 |
wenzelm |
support for context within morphism (for background theory);
|
file |
diff |
annotate
|
| Mon, 15 May 2023 20:55:17 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 15 May 2023 20:23:42 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 15 May 2023 20:19:02 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 21 Apr 2023 18:53:25 +0200 |
wenzelm |
more operations;
|
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
|
| Sat, 04 Sep 2021 21:25:08 +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, 03 Jun 2019 20:09:43 +0200 |
wenzelm |
clarified transfer_morphism: implicit join_certificate, e.g. relevant for complex cascades of morphisms such as class locale interpretation;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 22:05:25 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 21 Feb 2018 18:41:41 +0100 |
wenzelm |
explicit operations to instantiate frees: typ, term, thm, morphism;
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 14:49:11 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 18 Feb 2018 17:57:14 +0100 |
wenzelm |
more explicit instantiate_morphism (without checks for typ / term component);
|
file |
diff |
annotate
|
| Sun, 18 Feb 2018 16:31:56 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 02 Apr 2016 21:10:07 +0200 |
wenzelm |
careful export of type-dependent functions, without losing their special status;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2016 16:26:35 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2016 15:23:02 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 31 Aug 2015 19:04:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 13 Dec 2013 20:20:15 +0100 |
wenzelm |
maintain morphism names for diagnostic purposes;
|
file |
diff |
annotate
|