| Sun, 31 Dec 2023 22:04:41 +0100 |
wenzelm |
minor performance tuning: proper Same.operation;
|
file |
diff |
annotate
|
| Sun, 31 Dec 2023 19:24:37 +0100 |
wenzelm |
minor performance tuning: proper Same.operation;
|
file |
diff |
annotate
|
| Sun, 31 Dec 2023 16:15:27 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2023 22:36:41 +0100 |
wenzelm |
clarified signature: more operations;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2023 17:19:31 +0100 |
wenzelm |
clarified signature: prefer Same.operation;
|
file |
diff |
annotate
|
| Fri, 29 Dec 2023 15:58:43 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 22 Dec 2023 21:03:16 +0100 |
wenzelm |
clarified signature: downgrade old-style Global_Theory.add_defs to Global_Theory.add_def without attributes;
|
file |
diff |
annotate
|
| Mon, 18 Dec 2023 12:57:59 +0100 |
wenzelm |
minor performance tuning: more concise union;
|
file |
diff |
annotate
|
| Thu, 14 Dec 2023 17:33:45 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2023 13:03:10 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 10 Dec 2023 13:39:40 +0100 |
wenzelm |
more general Logic.incr_indexes_operation;
|
file |
diff |
annotate
|
| Sat, 09 Dec 2023 20:05:13 +0100 |
wenzelm |
clarified signature: fewer tuples;
|
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, 07 Dec 2023 10:46:49 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 02 Dec 2023 19:57:57 +0100 |
wenzelm |
clarified proof_body: cover zboxes from zproof;
|
file |
diff |
annotate
|
| Sat, 02 Dec 2023 15:42:50 +0100 |
wenzelm |
pro-forma support for optional zproof: no proper content yet;
|
file |
diff |
annotate
|
| Tue, 18 Apr 2023 12:04:41 +0200 |
wenzelm |
backout e3fe192fa4a8;
|
file |
diff |
annotate
|
| Tue, 18 Apr 2023 11:58:12 +0200 |
wenzelm |
backout 61f652dd955a;
|
file |
diff |
annotate
|
| Fri, 14 Apr 2023 22:19:28 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 11 Apr 2023 20:32:04 +0200 |
wenzelm |
performance tuning: replace Ord_List by Table();
|
file |
diff |
annotate
|
| Tue, 11 Apr 2023 15:03:02 +0200 |
wenzelm |
performance tuning: replace Ord_List by Set();
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 22:17:15 +0200 |
wenzelm |
tuned signature;
|
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
|
| Mon, 02 Dec 2019 15:04:38 +0100 |
wenzelm |
proper spec_rule name via naming/binding/Morphism.binding;
|
file |
diff |
annotate
|
| Sun, 01 Dec 2019 15:38:36 +0100 |
wenzelm |
proper spec rules via resulting def_thm, e.g. relevant for "isabelle build -o export_theory";
|
file |
diff |
annotate
|
| Fri, 29 Nov 2019 20:57:04 +0100 |
wenzelm |
more informative spec rules: optional name;
|
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
|
| Fri, 11 Oct 2019 22:01:45 +0200 |
wenzelm |
proper ML names;
|
file |
diff |
annotate
|
| Fri, 11 Oct 2019 21:23:06 +0200 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|