src/Pure/Isar/proof.ML
7 months ago wenzelm 2017-12-07 clarified document preparation vs. skip_proofs;
7 months ago wenzelm 2017-12-03 discontinued old 'def' command;
15 months ago wenzelm 2017-04-10 tuned signature;
19 months ago wenzelm 2016-12-14 always close derivation, for significantly improved performance without parallel proofs;
21 months ago wenzelm 2016-10-27 avoid multiple PIDE markup due to (potentially infinite) backtracking;
24 months ago wenzelm 2016-07-22 more markup for unstructured calculation;
2016-07-13 wenzelm 2016-07-13 obsolete;
2016-07-05 wenzelm 2016-07-05 PIDE reports of implicit variable scope;
2016-07-04 wenzelm 2016-07-04 clarified fact position, notably for reports on literal facts;
2016-07-04 wenzelm 2016-07-04 more accurate facts index;
2016-07-04 wenzelm 2016-07-04 tuned signature;
2016-06-23 wenzelm 2016-06-23 tuned signature;
2016-06-22 wenzelm 2016-06-22 tuned signature; tuned;
2016-06-07 wenzelm 2016-06-07 clean facts more uniformly;
2016-06-07 wenzelm 2016-06-07 tuned;
2016-04-26 wenzelm 2016-04-26 more uniform operations for structured statements;
2016-04-26 wenzelm 2016-04-26 defs are closed, which leads to proper auto_bind_facts; misc tuning;
2016-04-25 wenzelm 2016-04-25 clarified def binding position: reset for implicit/derived binding, keep for explicit binding;
2016-04-24 wenzelm 2016-04-24 added Isar command 'define';
2016-04-17 wenzelm 2016-04-17 clarified signature;
2016-04-15 wenzelm 2016-04-15 clarified PIDE reports;
2016-04-12 wenzelm 2016-04-12 back to static Mixfix.default_constraint without any special tricks (reverting e6443edaebff);
2016-04-02 wenzelm 2016-04-02 careful export of type-dependent functions, without losing their special status;
2016-03-30 wenzelm 2016-03-30 more explicit support for object-logic constraint;
2016-03-30 wenzelm 2016-03-30 more accurate mixfix type constraints;
2016-03-18 wenzelm 2016-03-18 clarified modules; tuned signature;
2015-12-13 wenzelm 2015-12-13 more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
2015-11-13 wenzelm 2015-11-13 preserve names of for-fixes for faithfully;
2015-11-13 wenzelm 2015-11-13 avoid vacuous quantification, as usual for shared variable scope;
2015-11-13 wenzelm 2015-11-13 support for structure statements in 'assume', 'presume';
2015-10-23 wenzelm 2015-10-23 clarified modules; tuned signature;
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-09-03 wenzelm 2015-09-03 proper restore_naming after global qed, which is important to make Name_Space.transform_naming work properly, e.g. for "private typedef";
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-01 wenzelm 2015-07-01 support for subgoal focus command;
2015-06-30 wenzelm 2015-06-30 renamed "default" to "standard", to make semantically clear what it is;
2015-06-29 wenzelm 2015-06-29 clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c); apply_end cases are no longer seen in current context section (hardly relevant in practice);
2015-06-27 wenzelm 2015-06-27 premises in 'show' are treated like 'assume';
2015-06-25 wenzelm 2015-06-25 tuned signature;
2015-06-24 wenzelm 2015-06-24 clarified 'case' command;
2015-06-22 wenzelm 2015-06-22 support 'when' statement, which corresponds to 'presume';
2015-06-22 wenzelm 2015-06-22 clarified nesting of Isar goal structure; tuned message;
2015-06-22 wenzelm 2015-06-22 tuned;
2015-06-14 wenzelm 2015-06-14 tuned signature;
2015-06-13 wenzelm 2015-06-13 tuned signature;
2015-06-13 wenzelm 2015-06-13 renamed "prems" to "that";
2015-06-11 wenzelm 2015-06-11 made SML/NJ happy;
2015-06-10 wenzelm 2015-06-10 prefer direct Assumption.add_assms -- avoid term bindings of Proof_Context.add_assms;
2015-06-10 wenzelm 2015-06-10 clarified local after_qed: result is not exported yet; proper goal_export for show: 'if' is like 'assume';
2015-06-10 wenzelm 2015-06-10 support for "if prems" in local goal statements;
2015-06-10 wenzelm 2015-06-10 no need for protected goal (see 240ad53041c9);
2015-06-10 wenzelm 2015-06-10 prevent export of future result -- avoid interference with goal fixes;
2015-06-09 wenzelm 2015-06-09 more uniform treatment of auto bindings vs. explicit user bindings; misc tuning;
2015-06-09 wenzelm 2015-06-09 tuned signature;
2015-06-09 wenzelm 2015-06-09 allow for_fixes for 'have', 'show' etc.; tuned signature;
2015-06-09 wenzelm 2015-06-09 tuned signature;
2015-06-09 wenzelm 2015-06-09 tuned;
2015-06-09 wenzelm 2015-06-09 clarified term bindings;