src/Pure/goal.ML
2016-12-14 wenzelm 2016-12-14 always close derivation, for significantly improved performance without parallel proofs;
2016-12-13 wenzelm 2016-12-13 more symbols;
2015-10-30 wenzelm 2015-10-30 tuned signature -- clarified modules;
2015-10-23 wenzelm 2015-10-23 clarified modules; tuned signature;
2015-08-16 wenzelm 2015-08-16 prefer theory_id operations; tuned signature;
2015-07-28 wenzelm 2015-07-28 proper context;
2015-07-14 wenzelm 2015-07-14 more aggressive compaction of multi-goal proof terms (see also a8babbb6d5ea, 4dd0ba632e40);
2015-07-14 wenzelm 2015-07-14 normalize proof before splitting conjunctions, according to Proof.conclude_goal (see also 4dd0ba632e40) -- may reduce general resource usage;
2015-07-08 wenzelm 2015-07-08 Variable.focus etc.: optional bindings provided by user; Subgoal.focus command: more careful treatment of user-provided bindings;
2015-07-05 wenzelm 2015-07-05 simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-05 wenzelm 2015-03-05 tuned -- more explicit use of context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-23 wenzelm 2015-02-23 Goal.prove_multi is superseded by the fully general Goal.prove_common;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2014-11-08 wenzelm 2014-11-08 optional proof context for unify operations, for the sake of proper local options;
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-08-19 wenzelm 2014-08-19 clarified modules;
2014-08-19 wenzelm 2014-08-19 added PARALLEL_ALLGOALS convenience;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-02-18 wenzelm 2014-02-18 tuned message;
2014-01-11 wenzelm 2014-01-11 reactivate Thm.check_hyps, after adapting AFP/Datatype_Order_Generator (see AFP/b7e389b5765c);
2014-01-11 wenzelm 2014-01-11 check_hyps for attribute application (still inactive, due to non-compliant tools); bypass check_hyps for locale expressions, where assumptions are not necessarily declared in intermediate situations;
2014-01-11 wenzelm 2014-01-11 clarified context;
2014-01-10 wenzelm 2014-01-10 disable Thm.check_hyps for now, due to remaining problems with AFP/Datatype_Order_Generator and AFP/Psi_Calculi (because of HOL-Nominal 'equivariance');
2014-01-10 wenzelm 2014-01-10 more elementary management of declared hyps, below structure Assumption; Goal.prove: insist in declared hyps; Simplifier: declare hyps via Thm.assume_hyps; more accurate tool context in some boundary cases;
2014-01-10 wenzelm 2014-01-10 explicit check of background theory;
2013-12-31 wenzelm 2013-12-31 proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-11-23 wenzelm 2013-11-23 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;
2013-08-25 wenzelm 2013-08-25 maintain goal forks as part of global execution; tuned;
2013-08-25 wenzelm 2013-08-25 simplified Goal.forked_proofs: status is determined via group instead of dummy future (see also Pure/PIDE/execution.ML); clarified Task_Queue.group_status; tuned;
2013-08-25 wenzelm 2013-08-25 discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information); simplified Goal.future_enabled;
2013-07-31 wenzelm 2013-07-31 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);
2013-07-29 wenzelm 2013-07-29 keep memo_exec execution running, which is important to cancel goal forks eventually; run as nested worker task to keep main group valid, even after cancelation of removed subgroups; do not memoize interrupt, but absorb it silently in main execution; Goal.purge_futures: rough sanity check of group status;
2013-07-29 wenzelm 2013-07-29 actually purge removed goal futures -- avoid memory leak;
2013-07-29 wenzelm 2013-07-29 tuned -- less redundant data structure;
2013-07-29 wenzelm 2013-07-29 discontinued notion of "stable" result -- running execution is never canceled;
2013-07-27 wenzelm 2013-07-27 clarified Goal.stable_futures after 00170ef1dc39: running tasks are considered stable, without potentially blocking join;
2013-07-27 wenzelm 2013-07-27 standardized aliases;
2013-07-19 wenzelm 2013-07-19 just one option "skip_proofs", without direct access within the editor (it makes document processing stateful without strong reasons -- monotonic updates already handle goal forks smoothly);
2013-07-18 wenzelm 2013-07-18 immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance;
2013-07-12 wenzelm 2013-07-12 clarified execution: maintain running execs only, check "stable" separately via memo (again); tuned signatures;
2013-07-02 wenzelm 2013-07-02 clarified Proofterm.proofs vs. Goal.skip_proofs;
2013-06-27 wenzelm 2013-06-27 more scalable PARALLEL_GOALS, using more elementary retrofit; tuned signature;
2013-06-26 wenzelm 2013-06-26 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context; even less intrusive PREFER_GOAL (without structural goal marker), e.g. relevant for generic_simp_tac; adapted ZF proof that broke for unknown reasons (potentially slight change of Drule.size_of_thm);
2013-06-26 wenzelm 2013-06-26 tuned signature;
2013-05-29 wenzelm 2013-05-29 tuned signature -- more explicit flags for low-level Thm.bicompose;
2013-05-21 wenzelm 2013-05-21 proper options;
2013-05-17 wenzelm 2013-05-17 proper option quick_and_dirty;
2013-05-13 wenzelm 2013-05-13 retain goal display options when printing error messages, to avoid breakdown for huge goals;
2013-04-03 wenzelm 2013-04-03 tuned;
2013-04-03 wenzelm 2013-04-03 recover implicit thread position for status messages (cf. eca8acb42e4a);
2013-04-03 wenzelm 2013-04-03 more explicit Goal.fork_params -- avoid implicit arguments via thread data; actually fork terminal proofs in interactive mode (amending 8707df0b0255);
2013-03-27 wenzelm 2013-03-27 more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
2013-03-27 wenzelm 2013-03-27 clarified Skip_Proof.cheat_tac: more standard tactic; clarified Method.cheating: check quick_and_dirty when it is actually applied;
2013-03-27 wenzelm 2013-03-27 tuned signature and module arrangement;
2013-03-13 wenzelm 2013-03-13 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate); clarified unknown timing vs. zero timing; tuned;