src/Pure/Isar/proof.ML
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;
2008-09-29 wenzelm 2008-09-29 promise global proofs;
2008-09-26 wenzelm 2008-09-26 eliminated polymorphic equality;
2008-09-18 wenzelm 2008-09-18 show: non-critical testing;
2008-09-17 wenzelm 2008-09-17 added map_contexts;
2008-09-02 wenzelm 2008-09-02 type Attrib.binding abbreviates Name.binding without attributes; Attrib.no_binding refers to Name.no_binding;
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements;
2008-05-16 wenzelm 2008-05-16 removed obsolete case rule_context;
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2008-03-11 wenzelm 2008-03-11 put_facts: do_props, i.e. facts are indexed by proposition again;
2008-01-24 wenzelm 2008-01-24 statement: keep explicit position; replaced ContextPosition by Position.thread_data;
2007-10-29 wenzelm 2007-10-29 test_proof: do not change Proofterm.proofs here (not thread-safe);
2007-10-11 wenzelm 2007-10-11 moved ProofContext.pp to Syntax.pp;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-10-01 wenzelm 2007-10-01 ContextPosition.put_ctxt;
2007-09-07 wenzelm 2007-09-07 reset goal messages after goal update;
2007-09-07 wenzelm 2007-09-07 made smlnj happy;
2007-09-06 wenzelm 2007-09-06 added goal_message;
2007-07-29 wenzelm 2007-07-29 renamed Drule.is_dummy_thm to Thm.is_dummy;
2007-07-27 wenzelm 2007-07-27 chain/using: filter out dummy_thm;
2007-07-24 wenzelm 2007-07-24 moved exception capture/release to structure Exn;
2007-07-13 wenzelm 2007-07-13 tuned;
2007-07-11 berghofe 2007-07-11 Proof terms for meta-conjunctions are now normalized before splitting up the conjunctions.
2007-07-07 wenzelm 2007-07-07 pretty_state: subgoal markup; tuned;
2007-06-19 wenzelm 2007-06-19 balanced conjunctions;
2007-06-13 wenzelm 2007-06-13 apply_method/end_proof: pass position; Method.Basic: include position;
2006-12-09 wenzelm 2006-12-09 init_context: reset naming;
2006-12-07 wenzelm 2006-12-07 reorganized structure Goal vs. Tactic;
2006-12-05 wenzelm 2006-12-05 generic_goal: enable stmt mode;
2006-11-28 wenzelm 2006-11-28 simplified '?' operator;
2006-11-22 wenzelm 2006-11-22 init: enter inner statement mode, which prevents local notes from being named internally;
2006-11-21 wenzelm 2006-11-21 made SML/NJ happy;
2006-11-21 wenzelm 2006-11-21 removed obsolete simple_note_thms;
2006-11-21 wenzelm 2006-11-21 simplified theorem(_i); notes: proper kind; renamed put_thms_internal to put_thms;
2006-11-14 wenzelm 2006-11-14 simplified Proof.theorem(_i) interface -- removed target support; removed obsolete global_goal interface; removed goal_names, simplified goal kind output; tuned;
2006-11-09 wenzelm 2006-11-09 Stack.map_top;
2006-10-09 wenzelm 2006-10-09 def(_i): LocalDefs.add_defs; removed Drule.strip_shyps_warning;
2006-10-07 wenzelm 2006-10-07 tuned;
2006-08-09 wenzelm 2006-08-09 global goals/qeds: after_qed operates on Proof.context (potentially local_theory);