| 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
|
| Sun, 16 Aug 2015 20:25:12 +0200 |
wenzelm |
produce certified vars without access to theory_of_thm, and without context;
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 19:25:08 +0200 |
wenzelm |
added Thm.chyps_of;
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 18:19:30 +0200 |
wenzelm |
prefer theory_id operations;
|
file |
diff |
annotate
|
| Sat, 15 Aug 2015 20:27:23 +0200 |
wenzelm |
obsolete;
|
file |
diff |
annotate
|
| Tue, 28 Jul 2015 19:49:54 +0200 |
wenzelm |
more direct access to atomic cterms;
|
file |
diff |
annotate
|
| Sun, 05 Jul 2015 15:02:30 +0200 |
wenzelm |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
file |
diff |
annotate
|
| Fri, 03 Jul 2015 14:32:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 30 May 2015 21:52:37 +0200 |
wenzelm |
more explicit context;
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 16:24:22 +0200 |
wenzelm |
explicitly checked alpha conversion -- actual renaming happens outside kernel;
|
file |
diff |
annotate
|