src/Pure/Isar/proof.ML
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.;
2009-07-20 ago moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
2009-07-20 ago Proof.future_proof: declare all assumptions as well;
2009-07-19 ago parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
2009-07-19 ago more abstract Future.is_worker;
2009-03-28 ago renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-28 ago renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
2009-03-28 ago simplified references to facts, eliminated external note_thmss;
2009-03-28 ago replaced add_binds(_i) by bind_terms -- internal version only;
2009-03-17 ago 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 ago unified type Proof.method and pervasive METHOD combinators;
2009-03-10 ago invoke_case: proper qualification of name binding, avoiding old no_base_names;
2009-03-05 ago eliminated obsolete ProofContext.full_bname;
2009-03-03 ago Thm.binding;
2009-01-21 ago binding is alias for Binding.T
2009-01-11 ago added Goal.future_enabled abstraction -- now also checks that this is already
2009-01-10 ago added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
2009-01-08 ago tuned;
2009-01-08 ago made SML/NJ happy
2009-01-07 ago future_proof: refined version covers local_future_proof and global_future_proof;
2009-01-07 ago qed/after_qed: singleton result;
2009-01-07 ago future_terminal_proof: no fork for interactive mode, assert_backward;
2009-01-06 ago future_terminal_proof: check Future.enabled;
2009-01-05 ago added future_terminal_proof;
2009-01-04 ago more precise is_relevant: requires original main goal, not initial goal state;
2008-12-12 ago global_qed: refrain from ProofContext.auto_bind_facts, to avoid
2008-12-05 ago merged