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;
2009-03-10 wenzelm 2009-03-10 invoke_case: proper qualification of name binding, avoiding old no_base_names;
2009-03-05 wenzelm 2009-03-05 eliminated obsolete ProofContext.full_bname;
2009-03-03 wenzelm 2009-03-03 Thm.binding;
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2009-01-11 wenzelm 2009-01-11 added Goal.future_enabled abstraction -- now also checks that this is already a future task, which excludes interactive commands of the old toplevel;
2009-01-10 wenzelm 2009-01-10 added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
2009-01-08 wenzelm 2009-01-08 tuned;
2009-01-08 haftmann 2009-01-08 made SML/NJ happy
2009-01-07 wenzelm 2009-01-07 future_proof: refined version covers local_future_proof and global_future_proof; future_proof: refrain from full Variable.auto_fixes -- not all contexts in the stack are in body mode; refined is_relevant: mode check; added local/global_future_terminal_proof;
2009-01-07 wenzelm 2009-01-07 qed/after_qed: singleton result;
2009-01-07 wenzelm 2009-01-07 future_terminal_proof: no fork for interactive mode, assert_backward;
2009-01-06 wenzelm 2009-01-06 future_terminal_proof: check Future.enabled;
2009-01-05 wenzelm 2009-01-05 added future_terminal_proof;
2009-01-04 wenzelm 2009-01-04 more precise is_relevant: requires original main goal, not initial goal state; tuned future_proof: minimal modification of goal state, retain original maxidx; tuned;
2008-12-12 wenzelm 2008-12-12 global_qed: refrain from ProofContext.auto_bind_facts, to avoid polluting the final result context with bindings involving loose free variables;
2008-12-05 wenzelm 2008-12-05 merged
2008-12-04 wenzelm 2008-12-04 future proofs: pass actual futures to facilitate composite computations;
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-10-16 wenzelm 2008-10-16 conclude_goal: precise goal context, include all sorts from context into statement, check shyps of result;
2008-10-02 wenzelm 2008-10-02 simplified Exn.EXCEPTIONS;
2008-10-01 wenzelm 2008-10-01 replaced can_defer by is_relevant (negation); future_proof: declare forked goal to prevent accidental generalization (e.g. instance goal);
2008-10-01 wenzelm 2008-10-01 future_proof: protect conclusion of deferred proof state;
2008-10-01 wenzelm 2008-10-01 renamed promise to future, tuned related interfaces;
2008-10-01 wenzelm 2008-10-01 more robust treatment of Interrupt (cf. exn.ML);
2008-09-30 wenzelm 2008-09-30 promise_proof: proper statement with empty vars;