| Sat, 30 Nov 2024 13:41:38 +0100 |
wenzelm |
tuned: more direct use of Name.context operations;
|
file |
diff |
annotate
|
| Fri, 29 Nov 2024 11:26:17 +0100 |
wenzelm |
tuned: more standard Name.build_context, although that is a bit longer;
|
file |
diff |
annotate
|
| Fri, 29 Nov 2024 00:25:03 +0100 |
wenzelm |
clarified signature: more uniform;
|
file |
diff |
annotate
|
| Sun, 04 Aug 2024 16:56:28 +0200 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Fri, 19 Jul 2024 16:58:52 +0200 |
wenzelm |
clarified thm_header command_pos vs. thm_pos;
|
file |
diff |
annotate
|
| Fri, 07 Jun 2024 23:53:31 +0200 |
wenzelm |
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
|
file |
diff |
annotate
|
| Sun, 31 Dec 2023 22:04:41 +0100 |
wenzelm |
minor performance tuning: proper Same.operation;
|
file |
diff |
annotate
|
| Sun, 31 Dec 2023 15:09:04 +0100 |
wenzelm |
pro-forma support for ZTerm.sorts_zproof;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2023 14:48:58 +0100 |
wenzelm |
misc tuning and clarification, following Term.incr_bv / Term.incr_boundvars;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2021 12:33:14 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 22:17:15 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 21:25:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 14:18:44 +0200 |
wenzelm |
more scalable operations;
|
file |
diff |
annotate
|
| Fri, 15 May 2020 08:40:28 +0200 |
Manuel Eberl |
added missing preprocessing step for extraction (due to Stefan Berghofer)
|
file |
diff |
annotate
|
| Tue, 21 Apr 2020 22:19:59 +0200 |
wenzelm |
clarified signature: avoid clash with Isabelle/Scala Term.OFCLASS on case-insensible file-system;
|
file |
diff |
annotate
|
| Fri, 08 Nov 2019 16:25:18 +0100 |
wenzelm |
more robust;
|
file |
diff |
annotate
|
| Sun, 20 Oct 2019 20:38:22 +0200 |
wenzelm |
clarified expand_proof/expand_name: allow more detailed control via thm_header;
|
file |
diff |
annotate
|
| Tue, 15 Oct 2019 13:30:02 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 11 Oct 2019 22:01:45 +0200 |
wenzelm |
proper ML names;
|
file |
diff |
annotate
|
| Fri, 11 Oct 2019 21:34:37 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 11 Oct 2019 21:23:06 +0200 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
| Thu, 10 Oct 2019 15:18:40 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 09 Aug 2019 15:58:26 +0200 |
wenzelm |
clarified ML types;
|
file |
diff |
annotate
|
| Fri, 02 Aug 2019 14:14:49 +0200 |
wenzelm |
more direct proofs for type classes;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2019 20:09:25 +0200 |
wenzelm |
clarified global theory context;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2019 14:35:29 +0200 |
wenzelm |
clarified modules: provide reconstruct_proof / expand_proof at the bottom of proof term construction;
|
file |
diff |
annotate
|
| Fri, 26 Jul 2019 14:43:56 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 26 Jul 2019 09:35:02 +0200 |
wenzelm |
defer rew_proof on unnamed PThm node as open_proof operation: significant performance improvement;
|
file |
diff |
annotate
|
| Sat, 09 Apr 2016 13:28:32 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|