src/Pure/Isar/proof.ML
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;
2009-11-02 wenzelm 2009-11-02 modernized structure Proof_Display;
2009-11-02 wenzelm 2009-11-02 modernized structure AutoBind;
2009-11-01 wenzelm 2009-11-01 modernized structure Rule_Cases;
2009-10-28 wenzelm 2009-10-28 replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;
2009-10-25 wenzelm 2009-10-25 more direct access to naming; tuned signature;
2009-10-20 wenzelm 2009-10-20 backpatching of structure Proof and ProofContext -- avoid odd aliases; renamed transfer_proof to raw_transfer; indicate firm naming conventions for theory, Proof.context, Context.generic;
2009-10-02 wenzelm 2009-10-02 clarified Proof.refine_insert -- always "refine" to apply standard method treatment (of conjunctions);
2009-09-30 wenzelm 2009-09-30 eliminated dead code;
2009-09-30 wenzelm 2009-09-30 replaced chained_goal by slightly more appropriate flat_goal;
2009-09-30 wenzelm 2009-09-30 added chained_goal, which presents the goal thm as seen by semi-structured methods;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-25 wenzelm 2009-07-25 basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context; Method.Basic: no position;
2009-07-25 wenzelm 2009-07-25 renamed structure Display_Goal to Goal_Display;
2009-07-24 wenzelm 2009-07-24 Display_Goal.pretty_goals: always Markup.subgoal, clarified options;
2009-07-23 wenzelm 2009-07-23 clarified pretty_goals, pretty_thm_aux: plain context; explicit pretty_goals_without_context, print_goals_without_context; tuned;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-20 wenzelm 2009-07-20 moved pretty_goals etc. to Display_Goal (required by tracing tacticals); load display.ML after assumption.ML, to accomodate proper contextual theorem display;
2009-07-20 wenzelm 2009-07-20 Proof.future_proof: declare all assumptions as well; Proof.future_proof: removed spurious exception_trace (which might cause crash-by-interrupt); replaced Future.fork_local by Future.fork_pri (again, until group exceptions are propagated properly);
2009-07-19 wenzelm 2009-07-19 parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
2009-07-19 wenzelm 2009-07-19 more abstract Future.is_worker; Future.fork_local: inherit from worker (if available);
2009-03-28 wenzelm 2009-03-28 renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-28 wenzelm 2009-03-28 renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
2009-03-28 wenzelm 2009-03-28 simplified references to facts, eliminated external note_thmss;
2009-03-28 wenzelm 2009-03-28 replaced add_binds(_i) by bind_terms -- internal version only;
2009-03-17 wenzelm 2009-03-17 goal_tac: finish marked assumptions from left to right -- corresponds better with the strategy of etac, with significant performance gains in some situations;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;