| 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
|