| Sat, 05 Jul 2025 16:01:40 +0200 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Sun, 09 Feb 2025 13:11:20 +0100 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Thu, 23 Jan 2025 20:46:26 +0100 |
wenzelm |
minor performance tuning: more fine-grained guard to skip irrelevant items;
|
file |
diff |
annotate
|
| Thu, 23 Jan 2025 20:06:14 +0100 |
wenzelm |
proper treatment of variables with the same name, but different sorts/types: this routinely happens in HOL Light (see also 0e2f019477e2), as well as theory "HOL-Algebra.Algebraic_Closure_Type" (line 77);
|
file |
diff |
annotate
|
| Wed, 22 Jan 2025 21:31:45 +0100 |
wenzelm |
tuned signature: more explicit operations;
|
file |
diff |
annotate
|
| Tue, 21 Jan 2025 15:48:39 +0100 |
wenzelm |
clarified exceptions;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2025 14:47:25 +0100 |
wenzelm |
more direct Thm.free: avoid re-certification;
|
file |
diff |
annotate
|
| Mon, 02 Dec 2024 20:35:12 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 29 Nov 2024 17:40:15 +0100 |
wenzelm |
clarified signature: shorten common cases;
|
file |
diff |
annotate
|
| Sun, 11 Aug 2024 11:32:20 +0200 |
wenzelm |
tuned modules;
|
file |
diff |
annotate
|
| Fri, 19 Jul 2024 16:58:52 +0200 |
wenzelm |
clarified thm_header command_pos vs. thm_pos;
|
file |
diff |
annotate
|
| Mon, 15 Jul 2024 12:26:15 +0200 |
wenzelm |
clarified signature: more operations;
|
file |
diff |
annotate
|
| Sun, 14 Jul 2024 15:16:08 +0200 |
wenzelm |
tuned signature;
|
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
|
| Fri, 07 Jun 2024 13:19:39 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 11 Jan 2024 12:37:10 +0100 |
wenzelm |
more uniform treatment of "hyps" within zproof;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2024 17:38:50 +0100 |
wenzelm |
clarified signature: avoid redundant Term.maxidx_of_term;
|
file |
diff |
annotate
|
| Mon, 08 Jan 2024 13:31:45 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 08 Jan 2024 12:08:31 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 06 Jan 2024 15:31:41 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 03 Jan 2024 12:40:10 +0100 |
wenzelm |
more operations (see also 8368160d3c65);
|
file |
diff |
annotate
|
| Mon, 01 Jan 2024 14:36:08 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 31 Dec 2023 21:40:14 +0100 |
wenzelm |
tuned signature;
|
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 15:09:04 +0100 |
wenzelm |
pro-forma support for ZTerm.sorts_zproof;
|
file |
diff |
annotate
|
| Sun, 31 Dec 2023 12:40:10 +0100 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Sun, 31 Dec 2023 12:22:23 +0100 |
wenzelm |
minor performance tuning: proper Same.operation;
|
file |
diff |
annotate
|
| Sun, 31 Dec 2023 11:50:05 +0100 |
wenzelm |
tuned names (again);
|
file |
diff |
annotate
|
| Sat, 30 Dec 2023 22:16:18 +0100 |
wenzelm |
tuned names;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2023 22:05:55 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2023 21:54:08 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2023 21:35:00 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2023 15:50:18 +0100 |
wenzelm |
more zproofs;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2023 12:12:43 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2023 11:26:05 +0100 |
wenzelm |
minor performance tuning, following 703201dbd413;
|
file |
diff |
annotate
|
| Wed, 27 Dec 2023 11:14:56 +0100 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Wed, 27 Dec 2023 11:10:51 +0100 |
wenzelm |
proper Thm.transfer;
|
file |
diff |
annotate
|
| Tue, 26 Dec 2023 22:14:44 +0100 |
wenzelm |
proper Thm.trim_context;
|
file |
diff |
annotate
|
| Tue, 26 Dec 2023 20:33:38 +0100 |
wenzelm |
clarified stored data: actual thm allows to replay zproofs in a modular manner;
|
file |
diff |
annotate
|
| Fri, 22 Dec 2023 17:19:08 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 22 Dec 2023 14:55:55 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 22 Dec 2023 13:53:03 +0100 |
wenzelm |
observe option "prune_proofs";
|
file |
diff |
annotate
|
| Thu, 21 Dec 2023 21:35:54 +0100 |
wenzelm |
clarified zproof storage: per-theory table in anticipation of session exports;
|
file |
diff |
annotate
|
| Thu, 21 Dec 2023 21:03:02 +0100 |
wenzelm |
proper thm_name for stored zproof;
|
file |
diff |
annotate
|
| Wed, 20 Dec 2023 20:58:56 +0100 |
wenzelm |
clarified context: avoid capture of thy2 within closure;
|
file |
diff |
annotate
|
| Wed, 20 Dec 2023 20:48:57 +0100 |
wenzelm |
tuned names;
|
file |
diff |
annotate
|
| Wed, 20 Dec 2023 20:28:55 +0100 |
wenzelm |
more informative exceptions;
|
file |
diff |
annotate
|
| Tue, 19 Dec 2023 22:56:32 +0100 |
wenzelm |
use strict Global_Theory.register_proofs as checkpoint for stored zproof, and thus reduce current zboxes;
|
file |
diff |
annotate
|
| Tue, 19 Dec 2023 19:18:09 +0100 |
wenzelm |
omit unclear / inaccurate renaming;
|
file |
diff |
annotate
|
| Tue, 19 Dec 2023 18:03:25 +0100 |
wenzelm |
more normalization: re-use Thm.solve_constraints as important checkpoint for results, notably Global_Theory.name_thm;
|
file |
diff |
annotate
|
| Tue, 19 Dec 2023 17:54:55 +0100 |
wenzelm |
more robust: avoid assumption about Context.certificate_theory;
|
file |
diff |
annotate
|
| Tue, 19 Dec 2023 17:31:12 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 19 Dec 2023 17:26:30 +0100 |
wenzelm |
clarified pro-forma proof: no zboxes here (partially revert 686b7b14d041);
|
file |
diff |
annotate
|
| Tue, 19 Dec 2023 17:07:22 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 19 Dec 2023 15:27:45 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 18 Dec 2023 12:57:59 +0100 |
wenzelm |
minor performance tuning: more concise union;
|
file |
diff |
annotate
|
| Sun, 17 Dec 2023 21:43:14 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 17 Dec 2023 21:12:18 +0100 |
wenzelm |
more robust norm_proof: turn env into instantiation, based on visible statement;
|
file |
diff |
annotate
|
| Thu, 14 Dec 2023 17:33:45 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 14 Dec 2023 12:21:09 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 13 Dec 2023 23:05:41 +0100 |
wenzelm |
more zproofs;
|
file |
diff |
annotate
|
| Wed, 13 Dec 2023 19:58:26 +0100 |
wenzelm |
more zproofs, imitating existing proofs (which are a bit rough here);
|
file |
diff |
annotate
|
| Wed, 13 Dec 2023 15:23:03 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Wed, 13 Dec 2023 14:58:49 +0100 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2023 22:08:43 +0100 |
wenzelm |
tuned comments (see also 476a239d3e0e and possibly 4b62e0cb3aa8);
|
file |
diff |
annotate
|
| Mon, 11 Dec 2023 21:31:58 +0100 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2023 21:17:28 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2023 21:09:24 +0100 |
wenzelm |
minor performance tuning: prefer Same.operation;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2023 20:53:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2023 19:33:31 +0100 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2023 14:26:24 +0100 |
wenzelm |
minor performance tuning: prefer Symset.T;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2023 12:45:16 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2023 12:27:42 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2023 12:06:18 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2023 11:50:50 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2023 11:46:12 +0100 |
wenzelm |
proper ZTerm.lift_proof (amending 4a1a25bdf81d);
|
file |
diff |
annotate
|
| Sun, 10 Dec 2023 13:39:40 +0100 |
wenzelm |
more general Logic.incr_indexes_operation;
|
file |
diff |
annotate
|
| Sun, 10 Dec 2023 11:42:57 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 09 Dec 2023 21:25:26 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 09 Dec 2023 20:37:36 +0100 |
wenzelm |
clarified signature: fewer tuples;
|
file |
diff |
annotate
|
| Sat, 09 Dec 2023 20:05:13 +0100 |
wenzelm |
clarified signature: fewer tuples;
|
file |
diff |
annotate
|
| Sat, 09 Dec 2023 17:31:10 +0100 |
wenzelm |
clarified signature: more explicit get_proofs_level with bounds check;
|
file |
diff |
annotate
|
| Fri, 08 Dec 2023 18:51:18 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 08 Dec 2023 18:40:31 +0100 |
wenzelm |
more zproofs;
|
file |
diff |
annotate
|
| Fri, 08 Dec 2023 16:01:42 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 08 Dec 2023 15:37:46 +0100 |
wenzelm |
more zproofs;
|
file |
diff |
annotate
|
| Fri, 08 Dec 2023 15:30:53 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2023 10:06:51 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2023 20:16:23 +0100 |
wenzelm |
more zproofs;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2023 16:04:00 +0100 |
wenzelm |
more zproofs;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2023 15:45:22 +0100 |
wenzelm |
more zproofs;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2023 15:32:53 +0100 |
wenzelm |
more zproofs;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2023 21:27:42 +0100 |
wenzelm |
more zproofs;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2023 20:56:51 +0100 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2023 20:07:52 +0100 |
wenzelm |
more zproofs;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2023 11:37:24 +0100 |
wenzelm |
more zproofs;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2023 11:02:05 +0100 |
wenzelm |
clarified const_proof vs. zproof_name;
|
file |
diff |
annotate
|
| Mon, 04 Dec 2023 23:07:06 +0100 |
wenzelm |
more zproofs;
|
file |
diff |
annotate
|
| Mon, 04 Dec 2023 10:53:32 +0100 |
wenzelm |
more zterm operations;
|
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, 06 Jun 2023 11:26:59 +0200 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Thu, 11 May 2023 12:21:50 +0200 |
wenzelm |
proper exception CONTEXT for Context.certificate_theory;
|
file |
diff |
annotate
|
| Fri, 05 May 2023 11:52:53 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Thu, 20 Apr 2023 12:44:19 +0200 |
wenzelm |
prefer theory_long_name in data;
|
file |
diff |
annotate
|
| Thu, 20 Apr 2023 11:57:34 +0200 |
wenzelm |
clarified signature: explicitly distinguish theory_base_name vs. theory_long_name;
|
file |
diff |
annotate
|
| Tue, 18 Apr 2023 21:03:24 +0200 |
wenzelm |
discontinued somewhat pointless operation: Conjunction.intr_balanced / Conjunction.elim_balanced with single hyp performs better (e.g. see AFP/351b7b576892);
|
file |
diff |
annotate
|
| Tue, 18 Apr 2023 18:27:22 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 18 Apr 2023 18:04:27 +0200 |
wenzelm |
backout b6aa5eac0a1a;
|
file |
diff |
annotate
|
| Tue, 18 Apr 2023 15:56:16 +0200 |
wenzelm |
Thm.shared context: speed-up low-level inferences;
|
file |
diff |
annotate
|
| Tue, 18 Apr 2023 12:45:01 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Tue, 18 Apr 2023 12:23:37 +0200 |
wenzelm |
backout 4a174bea55e2;
|
file |
diff |
annotate
|
| Tue, 18 Apr 2023 12:10:00 +0200 |
wenzelm |
Backed out changeset f34d11942ac1
|
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
|
| Tue, 18 Apr 2023 11:44:10 +0200 |
wenzelm |
Backed out changeset cd5d56abda10
|
file |
diff |
annotate
|
| Mon, 17 Apr 2023 23:32:46 +0200 |
wenzelm |
revert b43ee37926a9 due to problems with AFP/PAPP_Impossibility;
|
file |
diff |
annotate
|
| Tue, 11 Apr 2023 21:02:15 +0200 |
wenzelm |
tuned signature;
|
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
|
| Mon, 10 Apr 2023 22:38:18 +0200 |
wenzelm |
performance tuning: replace Ord_List by Set();
|
file |
diff |
annotate
|
| Mon, 10 Apr 2023 20:51:01 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 10 Apr 2023 19:37:15 +0200 |
wenzelm |
performance tuning: replace Ord_List by Table();
|
file |
diff |
annotate
|
| Mon, 10 Apr 2023 18:13:23 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 10 Apr 2023 18:08:23 +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, 31 Oct 2021 19:35:41 +0100 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Mon, 25 Oct 2021 17:37:24 +0200 |
wenzelm |
clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
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
|
| Wed, 13 Oct 2021 13:19:09 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 10 Sep 2021 14:59:19 +0200 |
wenzelm |
clarified signature: more scalable operations;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2021 15:45:27 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2021 12:33:14 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 06 Sep 2021 12:11:17 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 06 Sep 2021 11:32:18 +0200 |
wenzelm |
more efficient operations: traverse hyps only when required;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 22:17:15 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 22:05:35 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 21:45:43 +0200 |
wenzelm |
more scalable operations;
|
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
|
| Fri, 03 Sep 2021 14:34:14 +0200 |
wenzelm |
minor performance tuning: fewer allocations;
|
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
|
| Tue, 03 Aug 2021 13:08:23 +0200 |
wenzelm |
more uniform signatures in ML and Scala;
|
file |
diff |
annotate
|
| Fri, 18 Jun 2021 11:32:32 +0200 |
wenzelm |
tuned signature (see 2d6a489adb01);
|
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
|
| Sat, 14 Mar 2020 21:58:29 +0100 |
wenzelm |
more robust: proper transfer if Context.eq_thy_id;
|
file |
diff |
annotate
|
| Mon, 09 Mar 2020 15:38:52 +0100 |
wenzelm |
more thorough strip_shyps for proof boxes (but types are usually stripped and reconstructed later);
|
file |
diff |
annotate
|
| Mon, 09 Mar 2020 13:03:42 +0100 |
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, 17 Feb 2020 20:35:04 +0100 |
wenzelm |
proper sort constraints for strip_shyps, for sort relations used in minimization;
|
file |
diff |
annotate
|
| Mon, 17 Feb 2020 11:17:09 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 16 Feb 2020 17:24:10 +0100 |
wenzelm |
proper sort constraints for strip_shyps, which implicitly performs type instantiation;
|
file |
diff |
annotate
|
| Thu, 28 Nov 2019 18:13:23 +0100 |
wenzelm |
more structural integrity;
|
file |
diff |
annotate
|
| Fri, 08 Nov 2019 19:06:50 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 04 Nov 2019 14:56:49 +0100 |
wenzelm |
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
|
file |
diff |
annotate
|
| Sun, 03 Nov 2019 20:38:08 +0100 |
wenzelm |
expose derivations more thoroughly, notably for locale/class reasoning;
|
file |
diff |
annotate
|
| Sun, 03 Nov 2019 16:01:39 +0100 |
wenzelm |
more robust;
|
file |
diff |
annotate
|
| Sun, 03 Nov 2019 15:48:59 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 22 Oct 2019 20:55:13 +0200 |
wenzelm |
clarified axiom_table: uniform space (e.g. like consts), e.g. relevant for export of HOL-ex.Join_Theory;
|
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, 19 Oct 2019 15:32:32 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 11 Oct 2019 19:35:59 +0200 |
wenzelm |
proper treatment of axm_proof/oracle_proof like a closed proof constant, e.g. relevant for proof reconstruction of List.list.full_exhaustive_list.simps;
|
file |
diff |
annotate
|
| Fri, 11 Oct 2019 18:26:35 +0200 |
wenzelm |
clarified oracle_proof;
|
file |
diff |
annotate
|
| Thu, 10 Oct 2019 15:52:30 +0200 |
wenzelm |
proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);
|
file |
diff |
annotate
|
| Thu, 10 Oct 2019 15:10:07 +0200 |
wenzelm |
tuned -- more direct ML expressions;
|
file |
diff |
annotate
|
| Thu, 10 Oct 2019 15:00:36 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 10 Oct 2019 14:53:48 +0200 |
wenzelm |
more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;
|
file |
diff |
annotate
|
| Wed, 09 Oct 2019 22:52:34 +0200 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
| Wed, 09 Oct 2019 22:18:23 +0200 |
wenzelm |
tuned -- allow slightly more expensive atomic proofs;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2019 13:20:13 +0200 |
wenzelm |
clarified signature: prefer total operations;
|
file |
diff |
annotate
|
| Tue, 20 Aug 2019 18:39:33 +0200 |
wenzelm |
clarified thm_id vs. thm_node/thm: retain theory_name;
|
file |
diff |
annotate
|
| Tue, 20 Aug 2019 15:24:07 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 20 Aug 2019 15:12:06 +0200 |
wenzelm |
unused (see 095dadc62bb5);
|
file |
diff |
annotate
|
| Tue, 20 Aug 2019 11:28:29 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 20 Aug 2019 11:01:05 +0200 |
wenzelm |
clarified signature;
|
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:21:30 +0200 |
wenzelm |
added ML antiquotation @{oracle_name};
|
file |
diff |
annotate
|
| Sat, 17 Aug 2019 13:39:28 +0200 |
wenzelm |
more robust, notably for open_proof of unnamed derivation;
|
file |
diff |
annotate
|
| Sat, 17 Aug 2019 12:44:22 +0200 |
wenzelm |
added command 'thm_oracles';
|
file |
diff |
annotate
|
| Sat, 17 Aug 2019 11:39:29 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Sat, 17 Aug 2019 10:38:02 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 16 Aug 2019 21:02:18 +0200 |
wenzelm |
clarified identity of PThm nodes: do not reuse old id after renaming -- enforce uniqueness of substructures;
|
file |
diff |
annotate
|
| Fri, 16 Aug 2019 10:04:47 +0200 |
wenzelm |
clarified derivation_name vs. raw_derivation_name;
|
file |
diff |
annotate
|
| Mon, 12 Aug 2019 19:29:33 +0200 |
wenzelm |
more robust -- notably for metis, which tends to accumulate tpairs;
|
file |
diff |
annotate
|
| Sun, 11 Aug 2019 22:36:34 +0200 |
wenzelm |
record sort constraints unconditionally: minimal performance implications;
|
file |
diff |
annotate
|
| Fri, 09 Aug 2019 17:14:49 +0200 |
wenzelm |
formal position for PThm nodes;
|
file |
diff |
annotate
|
| Wed, 07 Aug 2019 15:48:52 +0200 |
wenzelm |
more robust and convenient treatment of implicit context;
|
file |
diff |
annotate
|
| Wed, 07 Aug 2019 10:52:19 +0200 |
wenzelm |
explicit check of left-over constraints from different theory, e.g. due to lack of Thm.trim_context;
|
file |
diff |
annotate
|
| Tue, 06 Aug 2019 19:47:46 +0200 |
wenzelm |
backed out changeset 1b8858f4c393: odd problems e.g. in CAVA_LTL_Modelchecker;
|
file |
diff |
annotate
|
| Tue, 06 Aug 2019 16:29:28 +0200 |
wenzelm |
more robust and convenient treatment of implicit context;
|
file |
diff |
annotate
|
| Mon, 05 Aug 2019 16:11:43 +0200 |
wenzelm |
clarified modules: more direct data implementation;
|
file |
diff |
annotate
|
| Sat, 03 Aug 2019 21:18:12 +0200 |
wenzelm |
more efficient data structure;
|
file |
diff |
annotate
|
| Sat, 03 Aug 2019 16:17:16 +0200 |
wenzelm |
guard constraints by record_proofs=1, until performance implications have become more clear;
|
file |
diff |
annotate
|
| Sat, 03 Aug 2019 16:10:34 +0200 |
wenzelm |
more complete completions according to Sorts.insert_complete_ars (cf. 13199740ced6), e.g. relevant for theories HOL-ex.Word_Type, HOL-Matrix_LP.SparseMatrix;
|
file |
diff |
annotate
|
| Sat, 03 Aug 2019 15:48:28 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 03 Aug 2019 15:05:53 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 03 Aug 2019 12:58:53 +0200 |
wenzelm |
maintain sort constraints from type instantiations, with pro-forma derivation to collect oracles/thms;
|
file |
diff |
annotate
|
| Fri, 02 Aug 2019 14:14:49 +0200 |
wenzelm |
more direct proofs for type classes;
|
file |
diff |
annotate
|
| Fri, 02 Aug 2019 11:43:36 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 02 Aug 2019 11:23:09 +0200 |
wenzelm |
clarified modules: inference kernel maintains sort algebra within the logic;
|
file |
diff |
annotate
|
| Thu, 01 Aug 2019 10:14:58 +0200 |
wenzelm |
clarified module structure;
|
file |
diff |
annotate
|
| Thu, 01 Aug 2019 09:55:37 +0200 |
wenzelm |
simplified module structure: back to plain datatype (see 95f4f08f950f and 70019ab5e57f);
|
file |
diff |
annotate
|
| Wed, 24 Jul 2019 11:32:18 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 23 Jul 2019 12:07:50 +0200 |
wenzelm |
proof terms are always constructed sequentially;
|
file |
diff |
annotate
|
| Mon, 03 Jun 2019 23:58:20 +0200 |
wenzelm |
more structural integrity;
|
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
|
| Sat, 13 Apr 2019 22:06:40 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 13 Apr 2019 19:58:28 +0200 |
wenzelm |
more ctyp operations;
|
file |
diff |
annotate
|
| Sat, 13 Apr 2019 16:56:12 +0200 |
wenzelm |
prefer exception TYPE, e.g. when used within conversion;
|
file |
diff |
annotate
|
| Sat, 13 Apr 2019 16:26:19 +0200 |
wenzelm |
tuned signature -- more ctyp operations;
|
file |
diff |
annotate
|
| Mon, 01 Oct 2018 16:41:36 +0200 |
wenzelm |
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
|
file |
diff |
annotate
|
| Fri, 27 Jul 2018 17:27:42 +0200 |
wenzelm |
proper maxidx: if x does not occur in A, its maxidx could get lost;
|
file |
diff |
annotate
|
| Fri, 27 Jul 2018 16:21:09 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 25 Feb 2018 15:44:46 +0100 |
wenzelm |
eliminated ASCII syntax from Pure bootstrap;
|
file |
diff |
annotate
|
| Wed, 21 Feb 2018 18:37:04 +0100 |
wenzelm |
more operations for ctyp, cterm;
|
file |
diff |
annotate
|
| Sun, 18 Feb 2018 15:05:21 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 02 Jan 2018 23:04:15 +0100 |
haftmann |
repaired whitespace accident from 2505cabfc515
|
file |
diff |
annotate
|
| Mon, 01 Jan 2018 20:42:08 +0000 |
haftmann |
proper namespace for evaluators
|
file |
diff |
annotate
|
| Thu, 22 Jun 2017 21:10:13 +0200 |
wenzelm |
consolidate proofs more simultaneously;
|
file |
diff |
annotate
|
| Mon, 10 Apr 2017 21:05:31 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 03 Feb 2017 23:24:45 +0100 |
wenzelm |
proper background certificate from make_context, which can be a super-theory of the direct join (amending d07464875dd4);
|
file |
diff |
annotate
|
| Fri, 16 Dec 2016 19:07:16 +0100 |
wenzelm |
consolidate nested thms with persistent result, for improved performance;
|
file |
diff |
annotate
|
| Fri, 16 Dec 2016 14:06:31 +0100 |
wenzelm |
tuned signature -- more abstract type thm_node;
|
file |
diff |
annotate
|
| Thu, 15 Dec 2016 21:16:10 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 15 Dec 2016 15:08:18 +0100 |
wenzelm |
back to full Proofterm.join_bodies, which was lost in 2011 (4e2abb045eac, cc53ce50f738);
|
file |
diff |
annotate
|
| Wed, 14 Dec 2016 18:22:18 +0100 |
wenzelm |
more careful derivation_closed / close_derivation;
|
file |
diff |
annotate
|
| Mon, 12 Sep 2016 20:31:28 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 05 Aug 2016 16:36:03 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sun, 30 Aug 2015 17:32:50 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 30 Aug 2015 15:43:13 +0200 |
wenzelm |
clarified exceptions;
|
file |
diff |
annotate
|
| Sun, 30 Aug 2015 15:21:25 +0200 |
wenzelm |
clarified exceptions;
|
file |
diff |
annotate
|
| Sun, 30 Aug 2015 12:17:23 +0200 |
wenzelm |
trim context for persistent storage;
|
file |
diff |
annotate
|
| Sun, 30 Aug 2015 11:56:37 +0200 |
wenzelm |
clarified exceptions;
|
file |
diff |
annotate
|
| Fri, 28 Aug 2015 23:48:03 +0200 |
wenzelm |
clarified exceptions: avoid interference of formal context failure with regular rule application failure (which is routinely handled in user-space);
|
file |
diff |
annotate
|
| Fri, 28 Aug 2015 23:21:04 +0200 |
wenzelm |
more abstract theory certificate, which is not necessarily the full theory;
|
file |
diff |
annotate
|
| Fri, 28 Aug 2015 13:37:06 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 28 Aug 2015 11:53:09 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 21:55:11 +0200 |
wenzelm |
produce certified vars without access to theory_of_thm, and without context;
|
file |
diff |
annotate
|