src/Pure/Isar/method.ML
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-03-07 wenzelm 2010-03-07 modernized structure Local_Defs;
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-11-01 wenzelm 2009-11-01 modernized structure Context_Rules;
2009-10-25 wenzelm 2009-10-25 make SML/NJ happy;
2009-10-24 wenzelm 2009-10-24 maintain explicit name space kind; export Name_Space.the_entry; tuned messages;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-24 wenzelm 2009-10-24 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-10-17 wenzelm 2009-10-17 Method.cheating: check quick_and_dirty here;
2009-10-17 wenzelm 2009-10-17 indicate CRITICAL nature of various setmp combinators;
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-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-05-30 wenzelm 2009-05-30 eliminated old Method.add_method(s);
2009-05-30 wenzelm 2009-05-30 removed obsolete combinators for method args;
2009-05-23 wenzelm 2009-05-23 removed some obsolete combinators for method args;
2009-03-18 wenzelm 2009-03-18 more precise type Symbol_Pos.text;
2009-03-17 wenzelm 2009-03-17 close/all_assm_tac: finish all subgoals from left to right (cf. Proof.goal_tac a28d83e903ce) -- NB: ALLGOALS/THEN_ALL_NEW operate from right to left;
2009-03-16 wenzelm 2009-03-16 adapted 'method_setup' command to Method.setup;
2009-03-15 wenzelm 2009-03-15 export section, sections; tuned signature;
2009-03-13 wenzelm 2009-03-13 simplified method setup;
2009-03-13 wenzelm 2009-03-13 added simplified setup; eliminated type Args.T; pervasive types 'a parser and 'a context_parser;
2009-03-13 wenzelm 2009-03-13 tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
2009-03-12 wenzelm 2009-03-12 renamed NameSpace.bind to NameSpace.define;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 wenzelm 2009-03-04 renamed Method.assumption_tac back to Method.assm_tac -- as assumption_tac it would have to be exactly the tactic behind the assumption method (with facts);
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-02-28 wenzelm 2009-02-28 moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
2009-02-11 kleing 2009-02-11 FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
2009-01-01 wenzelm 2009-01-01 assumption/close: discontinued implicit prems;
2008-12-05 haftmann 2008-12-05 removed Table.extend, NameSpace.extend_table
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token, renamed some operations; removed obsolete parse_args (cf. parse);
2008-08-06 wenzelm 2008-08-06 report markup;
2008-08-04 wenzelm 2008-08-04 tuned signature; eliminated obsolete pervasives;
2008-06-28 wenzelm 2008-06-28 replaced simple_text by fully-featured parse_args;
2008-06-16 wenzelm 2008-06-16 renamed rename_params_tac to rename_tac;
2008-06-16 wenzelm 2008-06-16 ML tactic: do not abstract over context again;
2008-05-14 wenzelm 2008-05-14 added intern, defined;
2008-04-29 haftmann 2008-04-29 added lemma antiquotation
2008-03-28 wenzelm 2008-03-28 ml_tactic: non-critical version via proof data and thread data;
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-28 wenzelm 2008-03-28 reorganized signature of ML_Context;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2008-03-26 wenzelm 2008-03-26 adapted to Context.thread_data interface;
2008-03-24 wenzelm 2008-03-24 ML runtime compilation: pass position, tuned signature;
2008-03-15 wenzelm 2008-03-15 tuned messages;
2008-01-24 wenzelm 2008-01-24 improved apply: handle thread position, apply to context here; replaced ContextPosition by Position.thread_position;
2007-12-18 wenzelm 2007-12-18 named some critical sections;
2007-11-02 haftmann 2007-11-02 generic tactic Method.intros_tac
2007-08-01 wenzelm 2007-08-01 tuned;
2007-07-28 wenzelm 2007-07-28 tuned;
2007-07-27 wenzelm 2007-07-27 method section scanners: added [[declaration]] syntax, ignore sid-effects of thms;
2007-07-23 wenzelm 2007-07-23 eliminated transform_failure (to avoid critical section for main transactions);
2007-07-23 wenzelm 2007-07-23 marked some CRITICAL sections (for multithreading);
2007-07-08 wenzelm 2007-07-08 replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
2007-07-05 wenzelm 2007-07-05 renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
2007-07-05 wenzelm 2007-07-05 avoid polymorphic equality;
2007-06-19 wenzelm 2007-06-19 added raw_tactic;