src/Pure/Isar/proof.ML
2015-06-07 wenzelm 2015-06-07 tuned signature;
2015-06-07 wenzelm 2015-06-07 tuned signature;
2015-06-05 wenzelm 2015-06-05 added Isar command 'supply';
2015-06-05 wenzelm 2015-06-05 clarified signature -- better support for Isar commands outside of Pure;
2015-04-16 wenzelm 2015-04-16 explicit error for Toplevel.proof_of; eliminated obsolete Toplevel.unknown_proof; more total Toplevel.proof_position_of;
2015-04-08 wenzelm 2015-04-08 proper context for Object_Logic operations;
2015-04-08 wenzelm 2015-04-08 tuned signature;
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-03-01 wenzelm 2015-03-01 added Proof_Context.cterm_of/ctyp_of convenience;
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-12-23 wenzelm 2014-12-23 tuned message;
2014-12-23 wenzelm 2014-12-23 explicit message channels for "state", "information"; separate state_message_color;
2014-12-19 wenzelm 2014-12-19 tuned;
2014-11-08 wenzelm 2014-11-08 optional proof context for unify operations, for the sake of proper local options;
2014-11-03 wenzelm 2014-11-03 eliminated obsolete Proof.goal_message -- print outcome more directly;
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-10-28 wenzelm 2014-10-28 'oops' requires proper goal statement -- exclude 'notepad' to avoid disrupting begin/end structure;
2014-10-28 wenzelm 2014-10-28 more abstract type;
2014-10-28 wenzelm 2014-10-28 tuned;
2014-08-19 wenzelm 2014-08-19 tuned signature -- moved type src to Token, without aliases;
2014-08-19 wenzelm 2014-08-19 just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
2014-08-19 wenzelm 2014-08-19 tuned;
2014-08-19 wenzelm 2014-08-19 clarifed Method.evaluate: turn text into semantic method (like Basic);
2014-08-19 wenzelm 2014-08-19 simplified type Proof.method;
2014-07-02 wenzelm 2014-07-02 check 'case' variable bindings as for 'fix', which means internal names are rejected as usual;
2014-05-09 wenzelm 2014-05-09 more markup;
2014-05-09 wenzelm 2014-05-09 more position markup to help locating the query context, e.g. from "Info" dockable;
2014-05-08 wenzelm 2014-05-08 some position markup to help locating the query context, e.g. from "Info" dockable;
2014-05-07 wenzelm 2014-05-07 tuned message: "step" goes back to TTY mode before Proof General, while "depth" is more informative but sometimes confusing due to implementation details;
2014-05-07 wenzelm 2014-05-07 print results as "state", to avoid intrusion into the source text; print new local theory (again);
2014-03-09 wenzelm 2014-03-09 tuned signature;
2014-03-08 wenzelm 2014-03-08 modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121); proper context for global data; tuned signature;
2014-03-06 wenzelm 2014-03-06 eliminated odd type constraint for read_const (see also 79c1d2bbe5a9);
2014-03-06 wenzelm 2014-03-06 more uniform check_const/read_const;
2014-02-26 wenzelm 2014-02-26 markup for method combinators;
2014-02-25 wenzelm 2014-02-25 modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion; removed obsolete Method.Source_i; proper context for global data; tuned messages;
2014-02-24 wenzelm 2014-02-24 clarified Token.range_of in accordance to Symbol_Pos.range; eliminated redundant Position.set_range, which is already included in Position.range;
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-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-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-09-03 wenzelm 2013-09-03 cases: formal binding of 'assumes', with position provided via invoke_case; allow literal equality on type Binding.binding;
2013-09-03 wenzelm 2013-09-03 cases: more position information and PIDE markup;
2013-08-25 wenzelm 2013-08-25 maintain goal forks as part of global execution; 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-27 wenzelm 2013-07-27 standardized aliases;
2013-07-13 wenzelm 2013-07-13 hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
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-04-09 wenzelm 2013-04-09 just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
2013-04-03 wenzelm 2013-04-03 additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
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-30 wenzelm 2013-03-30 more item markup; tuned signature;
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 tuned signature and module arrangement;
2013-03-09 wenzelm 2013-03-09 tuned;
2013-03-04 wenzelm 2013-03-04 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones; refined parallel_proofs = 3: fork terminal proofs, as poor man's parallelization in interactive mode;