src/Pure/Isar/proof.ML
2012-04-27 ago clarified signature;
2012-04-12 ago more precise declaration of goal_tfrees in forked proof state;
2012-04-10 ago static relevance of proof via syntax keywords;
2012-03-21 ago tuned signature;
2012-03-21 ago tuned messages;
2012-03-21 ago prefer explicitly qualified exception List.Empty;
2012-03-18 ago maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
2012-02-28 ago display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
2012-02-14 ago tuned signature, according to actual usage of these operations;
2011-11-28 ago separate module for concrete Isabelle markup;
2011-11-20 ago uniform cert_vars/read_vars;
2011-11-07 ago tuned signature -- avoid spurious Thm.mixed_attribute;
2011-11-03 ago tuned signature -- canonical argument order;
2011-08-01 ago infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
2011-07-11 ago tuned signature -- corresponding to Scala version;
2011-05-12 ago proper configuration options Proof_Context.debug and Proof_Context.verbose;
2011-04-27 ago more precise positions via binding;
2011-04-16 ago modernized structure Proof_Context;
2011-04-08 ago discontinued special treatment of structure Mixfix;
2011-03-21 ago tuned;
2011-01-31 ago more specific Goal.fork_name;
2010-12-15 ago 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 ago formal notepad without any result;
2010-11-22 ago added useful function map_context_result to signature
2010-10-25 ago renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
2010-09-22 ago renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
2010-09-09 ago more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
2010-09-04 ago recovered options for goal antiquotations from f45d332a90e3: actually pass context to Proof.pretty_goals (see also 45facd8f358e);
2010-09-03 ago 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 ago 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 ago added some proof state markup, notably number of subgoals (e.g. for indentation);
2010-08-11 ago removed obsolete Proof.get_thmss_cmd (cf. Attrib.eval_thms);
2010-08-06 ago 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 ago moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
2010-05-29 ago explicit markup for forked goals, as indicated by Goal.fork;
2010-04-29 ago 'write': actually observe the proof structure (like 'let' or 'fix');
2010-04-29 ago ProofContext.read_const: allow for type constraint (for fixed variable);
2010-04-26 ago eliminanated some unreferenced identifiers;
2010-04-25 ago removed obsolete/unused Proof.match_bind;
2010-04-25 ago modernized naming conventions of main Isar proof elements;
2010-04-25 ago goals: simplified handling of implicit variables -- removed obsolete warning;
2010-03-07 ago modernized structure Local_Defs;
2010-01-15 ago Eliminated is_open option of Rule_Cases.make_nested/make_common;
2010-01-04 ago after_qed: refrain from Position.setmp_thread_data, which causes duplication of results with several independent proof attempts;
2009-11-02 ago modernized structure Proof_Display;
2009-11-02 ago modernized structure AutoBind;
2009-11-01 ago modernized structure Rule_Cases;
2009-10-28 ago replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;
2009-10-25 ago more direct access to naming;
2009-10-20 ago backpatching of structure Proof and ProofContext -- avoid odd aliases;
2009-10-02 ago clarified Proof.refine_insert -- always "refine" to apply standard method treatment (of conjunctions);
2009-09-30 ago eliminated dead code;
2009-09-30 ago replaced chained_goal by slightly more appropriate flat_goal;
2009-09-30 ago added chained_goal, which presents the goal thm as seen by semi-structured methods;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-07-25 ago basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
2009-07-25 ago renamed structure Display_Goal to Goal_Display;
2009-07-24 ago Display_Goal.pretty_goals: always Markup.subgoal, clarified options;
2009-07-23 ago clarified pretty_goals, pretty_thm_aux: plain context;
2009-07-21 ago proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;