src/Pure/Isar/proof.ML
2012-10-16 wenzelm 2012-10-16 more proof method text position information;
2012-10-16 wenzelm 2012-10-16 clarified defer/prefer: more specific errors;
2012-10-16 wenzelm 2012-10-16 more informative errors for 'proof' and 'apply' steps; more Seq.result operations;
2012-10-16 wenzelm 2012-10-16 more informative error for stand-alone 'qed';
2012-10-16 wenzelm 2012-10-16 further attempts to unify/simplify goal output;
2012-10-16 wenzelm 2012-10-16 more informative error messages of initial/terminal proof methods; more systematic support for sequences with embedded errors; tuned Seq.maps;
2012-10-13 wenzelm 2012-10-13 more informative error of initial/terminal proof steps;
2012-10-13 wenzelm 2012-10-13 some attempts to unify/simplify pretty_goal;
2012-10-13 wenzelm 2012-10-13 refined Proof.the_finished_goal with more informative error; more permissive Method.all_assm_tac: do not insist in solving by assumption here to postpone failure; clarified Method.finish_text: no Thm.no_prems filtering here to postpone failure;
2012-10-09 wenzelm 2012-10-09 clarified Local_Defs.add_def(s): refrain from hard-wiring Thm.def_binding_optional; clarified Generic_Target.define: avoid duplicate def binding via Local_Defs.add_def;
2012-09-01 wenzelm 2012-09-01 removed unused material;
2012-09-01 wenzelm 2012-09-01 discontinued complicated/unreliable notion of recent proofs within context;
2012-08-31 wenzelm 2012-08-31 more precise register_proofs for local goals; tuned signature;
2012-08-30 wenzelm 2012-08-30 register proofs of Isar goals, to enable recovery from unstable command states after interactive cancellation;
2012-08-30 wenzelm 2012-08-30 refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390); stretched meaning of Goal.parallel_proofs to enable future_terminal_proofs in interactive document model, despite its lack for regular forking of proofs;
2012-08-30 wenzelm 2012-08-30 some support for registering forked proofs within Proof.state, using its bottom context; tuned signature;
2012-04-27 wenzelm 2012-04-27 clarified signature;
2012-04-12 wenzelm 2012-04-12 more precise declaration of goal_tfrees in forked proof state;
2012-04-10 wenzelm 2012-04-10 static relevance of proof via syntax keywords;
2012-03-21 wenzelm 2012-03-21 tuned signature;
2012-03-21 wenzelm 2012-03-21 tuned messages;
2012-03-21 wenzelm 2012-03-21 prefer explicitly qualified exception List.Empty;
2012-03-18 wenzelm 2012-03-18 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming); more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global); prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output); simplified signatures;
2012-02-28 wenzelm 2012-02-28 display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
2012-02-14 wenzelm 2012-02-14 tuned signature, according to actual usage of these operations;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-11-20 wenzelm 2011-11-20 uniform cert_vars/read_vars;
2011-11-07 wenzelm 2011-11-07 tuned signature -- avoid spurious Thm.mixed_attribute;
2011-11-03 wenzelm 2011-11-03 tuned signature -- canonical argument order;
2011-08-01 nipkow 2011-08-01 infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
2011-07-11 wenzelm 2011-07-11 tuned signature -- corresponding to Scala version;
2011-05-12 wenzelm 2011-05-12 proper configuration options Proof_Context.debug and Proof_Context.verbose; discontinued alias Proof.verbose = Proof_Context.verbose;
2011-04-27 wenzelm 2011-04-27 more precise positions via binding;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Mixfix; eliminated slightly odd no_syn convenience;
2011-03-21 wenzelm 2011-03-21 tuned;
2011-01-31 wenzelm 2011-01-31 more specific Goal.fork_name;
2010-12-15 wenzelm 2010-12-15 show: display goal refinement rule as "state", to avoid odd Output.urgent_message and make its association with the goal more explicit;
2010-12-04 wenzelm 2010-12-04 formal notepad without any result;
2010-11-22 bulwahn 2010-11-22 added useful function map_context_result to signature
2010-10-25 wenzelm 2010-10-25 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
2010-09-22 wenzelm 2010-09-22 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
2010-09-09 wenzelm 2010-09-09 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
2010-09-04 wenzelm 2010-09-04 recovered options for goal antiquotations from f45d332a90e3: actually pass context to Proof.pretty_goals (see also 45facd8f358e);
2010-09-03 wenzelm 2010-09-03 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
2010-09-03 wenzelm 2010-09-03 Proof.pretty_state: print everything in the foreground context to give users a chance to configure options, e.g. via "using [[show_consts]]";
2010-08-25 wenzelm 2010-08-25 added some proof state markup, notably number of subgoals (e.g. for indentation); tuned;
2010-08-11 wenzelm 2010-08-11 removed obsolete Proof.get_thmss_cmd (cf. Attrib.eval_thms);
2010-08-06 wenzelm 2010-08-06 removed obsolete Goal.local_future_enforced: Toplevel.run_command is no longer interactive, so Goal.local_future_enabled is sufficient (cf. 349e9223c685 and e07dacec79e7);
2010-07-24 wenzelm 2010-07-24 moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state; theory loader: reduced warnings -- thy database can be bypassed in certain situations; Proof/Local_Theory.propagate_ml_env; ML use function: propagate ML environment as well; pervasive type generic_theory;
2010-05-29 wenzelm 2010-05-29 explicit markup for forked goals, as indicated by Goal.fork; accumulate pending forks within command state and hilight accordingly; Isabelle_Process: enforce future_terminal_proof, which gives some impression of non-linear/parallel checking;
2010-04-29 wenzelm 2010-04-29 'write': actually observe the proof structure (like 'let' or 'fix');
2010-04-29 wenzelm 2010-04-29 ProofContext.read_const: allow for type constraint (for fixed variable); added proof command 'write' to introduce concrete syntax within a proof body;
2010-04-26 wenzelm 2010-04-26 eliminanated some unreferenced identifiers; tuned;
2010-04-25 wenzelm 2010-04-25 removed obsolete/unused Proof.match_bind;
2010-04-25 wenzelm 2010-04-25 modernized naming conventions of main Isar proof elements;
2010-04-25 wenzelm 2010-04-25 goals: simplified handling of implicit variables -- removed obsolete warning;
2010-03-07 wenzelm 2010-03-07 modernized structure Local_Defs;
2010-01-15 berghofe 2010-01-15 Eliminated is_open option of Rule_Cases.make_nested/make_common; use Rule_Cases.internalize_params to rename parameters instead.
2010-01-04 wenzelm 2010-01-04 after_qed: refrain from Position.setmp_thread_data, which causes duplication of results with several independent proof attempts;