| Sat, 08 Mar 2025 22:19:49 +0100 |
wenzelm |
proper documentation for ML antiquotation \<^instantiate>;
|
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
|
| Tue, 18 Apr 2023 12:23:37 +0200 |
wenzelm |
backout 4a174bea55e2;
|
file |
diff |
annotate
|
| Tue, 18 Apr 2023 12:04:41 +0200 |
wenzelm |
backout e3fe192fa4a8;
|
file |
diff |
annotate
|
| Tue, 11 Apr 2023 15:03:02 +0200 |
wenzelm |
performance tuning: replace Ord_List by Set();
|
file |
diff |
annotate
|
| Tue, 28 Mar 2023 17:59:54 +0200 |
wenzelm |
prefer Sortset.T for shyps;
|
file |
diff |
annotate
|
| Sun, 15 Jan 2023 18:30:18 +0100 |
wenzelm |
isabelle update -u cite;
|
file |
diff |
annotate
|
| Sun, 12 Dec 2021 11:18:42 +0100 |
wenzelm |
merged, resolving conflict in src/Doc/Implementation/Logic.thy;
|
file |
diff |
annotate
|
| Tue, 07 Dec 2021 19:32:43 +0100 |
wenzelm |
proper syntax category;
|
file |
diff |
annotate
|
| Sun, 05 Dec 2021 12:50:36 +0100 |
wenzelm |
clarified corner cases of syntax;
|
file |
diff |
annotate
|
| Fri, 03 Dec 2021 20:11:21 +0100 |
wenzelm |
more documentation about Type/Const antiquotations;
|
file |
diff |
annotate
|
| Thu, 28 Oct 2021 13:13:48 +0200 |
wenzelm |
local fixes for "lemma" antiquotation;
|
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
|
| Thu, 26 Aug 2021 14:45:19 +0200 |
wenzelm |
more scalable data structure (but: rarely used with > 5 arguments);
|
file |
diff |
annotate
|
| Sat, 22 May 2021 22:58:10 +0200 |
wenzelm |
more uniform document antiquotations for ML: consolidate former setup for manuals;
|
file |
diff |
annotate
|
| Sat, 22 May 2021 21:52:13 +0200 |
wenzelm |
clarified names;
|
file |
diff |
annotate
|
| Sat, 22 May 2021 13:35:25 +0200 |
wenzelm |
clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;
|
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
|
| Mon, 24 Feb 2020 20:57:29 +0100 |
wenzelm |
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
|
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
|
| Sat, 17 Aug 2019 17:59:55 +0200 |
wenzelm |
discontinued peek_status: unused and not clearly defined;
|
file |
diff |
annotate
|
| Sat, 17 Aug 2019 17:57:10 +0200 |
wenzelm |
more documentation on oracles;
|
file |
diff |
annotate
|