| Sat, 20 May 2023 16:12:37 +0200 |
wenzelm |
more robust context: fail immediately via Morphism.the_theory, instead of rarely via Thm.theory_of_thm (for non-normal thm);
|
file |
diff |
annotate
|
| Mon, 15 May 2023 14:09:45 +0200 |
wenzelm |
more operations "without_context", assuming that the thm has been properly transferred already;
|
file |
diff |
annotate
|
| Mon, 15 May 2023 10:59:49 +0200 |
wenzelm |
tuned: more accurate check (is_norm_hhf protect);
|
file |
diff |
annotate
|
| Tue, 18 Apr 2023 22:24:48 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2022 19:23:12 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 03 Sep 2022 23:10:38 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 03 Sep 2022 17:37:46 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 15 Oct 2021 22:00:28 +0200 |
wenzelm |
revert bbfed17243af, breaks HOL-Proofs extraction;
|
file |
diff |
annotate
|
| Fri, 15 Oct 2021 20:54:13 +0200 |
wenzelm |
proper context for Goal.prove_internal;
|
file |
diff |
annotate
|
| Fri, 10 Sep 2021 14:59:19 +0200 |
wenzelm |
clarified signature: more scalable operations;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2021 14:50:26 +0200 |
wenzelm |
clarified set of items with order of addition;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2021 12:33:14 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 06 Sep 2021 13:49:36 +0200 |
wenzelm |
more scalable operations;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 21:25:08 +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
|
| Fri, 09 Aug 2019 17:14:49 +0200 |
wenzelm |
formal position for PThm nodes;
|
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
|
| Tue, 23 Jul 2019 12:07:50 +0200 |
wenzelm |
proof terms are always constructed sequentially;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 14:12:44 +0100 |
wenzelm |
clarified signature: more types;
|
file |
diff |
annotate
|
| Fri, 27 Jul 2018 17:32:16 +0200 |
wenzelm |
proper adjust_maxidx: assms could have maxidx >= 0, e.g. from command "subgoal premises";
|
file |
diff |
annotate
|
| Wed, 09 May 2018 20:45:57 +0200 |
wenzelm |
clarified future scheduling parameters, with support for parallel_limit;
|
file |
diff |
annotate
|
| Tue, 24 Apr 2018 11:03:51 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 25 Feb 2018 15:44:46 +0100 |
wenzelm |
eliminated ASCII syntax from Pure bootstrap;
|
file |
diff |
annotate
|
| Mon, 10 Apr 2017 21:05:31 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 14 Dec 2016 16:59:41 +0100 |
wenzelm |
always close derivation, for significantly improved performance without parallel proofs;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2016 11:51:42 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Fri, 30 Oct 2015 17:14:30 +0100 |
wenzelm |
tuned signature -- clarified modules;
|
file |
diff |
annotate
|
| Fri, 23 Oct 2015 17:17:11 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 18:19:30 +0200 |
wenzelm |
prefer theory_id operations;
|
file |
diff |
annotate
|
| Tue, 28 Jul 2015 20:05:53 +0200 |
wenzelm |
proper context;
|
file |
diff |
annotate
|
| Tue, 14 Jul 2015 19:01:46 +0200 |
wenzelm |
more aggressive compaction of multi-goal proof terms (see also a8babbb6d5ea, 4dd0ba632e40);
|
file |
diff |
annotate
|
| Tue, 14 Jul 2015 11:29:43 +0200 |
wenzelm |
normalize proof before splitting conjunctions, according to Proof.conclude_goal (see also 4dd0ba632e40) -- may reduce general resource usage;
|
file |
diff |
annotate
|
| Wed, 08 Jul 2015 19:28:43 +0200 |
wenzelm |
Variable.focus etc.: optional bindings provided by user;
|
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, 06 Mar 2015 17:32:20 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 13:28:04 +0100 |
wenzelm |
tuned -- more explicit use of context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Mon, 23 Feb 2015 14:50:30 +0100 |
wenzelm |
Goal.prove_multi is superseded by the fully general Goal.prove_common;
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Mon, 10 Nov 2014 21:49:48 +0100 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
file |
diff |
annotate
|
| Sat, 08 Nov 2014 21:31:51 +0100 |
wenzelm |
optional proof context for unify operations, for the sake of proper local options;
|
file |
diff |
annotate
|
| Thu, 30 Oct 2014 16:20:46 +0100 |
wenzelm |
eliminated aliases;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 18:11:04 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 17:00:44 +0200 |
wenzelm |
added PARALLEL_ALLGOALS convenience;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 20:32:58 +0100 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Sat, 11 Jan 2014 21:39:21 +0100 |
wenzelm |
reactivate Thm.check_hyps, after adapting AFP/Datatype_Order_Generator (see AFP/b7e389b5765c);
|
file |
diff |
annotate
|
| Sat, 11 Jan 2014 20:06:31 +0100 |
wenzelm |
check_hyps for attribute application (still inactive, due to non-compliant tools);
|
file |
diff |
annotate
|
| Sat, 11 Jan 2014 17:05:03 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 10 Jan 2014 23:42:18 +0100 |
wenzelm |
disable Thm.check_hyps for now, due to remaining problems with AFP/Datatype_Order_Generator and AFP/Psi_Calculi (because of HOL-Nominal 'equivariance');
|
file |
diff |
annotate
|
| Fri, 10 Jan 2014 21:37:28 +0100 |
wenzelm |
more elementary management of declared hyps, below structure Assumption;
|
file |
diff |
annotate
|
| Fri, 10 Jan 2014 16:20:06 +0100 |
wenzelm |
explicit check of background theory;
|
file |
diff |
annotate
|
| Tue, 31 Dec 2013 14:29:16 +0100 |
wenzelm |
proper context for norm_hhf and derived operations;
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Sat, 23 Nov 2013 17:15:44 +0100 |
wenzelm |
more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal -- NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;
|
file |
diff |
annotate
|
| Sun, 25 Aug 2013 20:32:26 +0200 |
wenzelm |
maintain goal forks as part of global execution;
|
file |
diff |
annotate
|
| Sun, 25 Aug 2013 17:04:22 +0200 |
wenzelm |
simplified Goal.forked_proofs: status is determined via group instead of dummy future (see also Pure/PIDE/execution.ML);
|
file |
diff |
annotate
|
| Sun, 25 Aug 2013 16:03:12 +0200 |
wenzelm |
discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
|
file |
diff |
annotate
|
| Wed, 31 Jul 2013 13:00:42 +0200 |
wenzelm |
clarified priority of "skipped" proofs, which might take long but do not produce relevant information (potential conflict of quick interactive feedback vs. performance in batch mode);
|
file |
diff |
annotate
|