src/Pure/Isar/method.ML
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;
2007-06-14 wenzelm 2007-06-14 method assumption: uniform treatment of prems as legacy feature;
2007-06-13 wenzelm 2007-06-13 Basic text: include position; assumption/close: refer to non-atomic assumptions as well, implicit use of prems now considered legacy feature;
2007-05-31 wenzelm 2007-05-31 simplified/unified list fold;
2007-05-24 haftmann 2007-05-24 tuned Pure/General/name_space.ML
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-04 wenzelm 2007-04-04 tuned comment;
2007-01-20 wenzelm 2007-01-20 ML tactic: proper context for compile and runtime;
2007-01-19 wenzelm 2007-01-19 removed obsolete Method; added parse (from outer_parse.ML); moved ML context stuff to from Context to ML_Context; tactic: no need to rebind thm/thms;
2007-01-19 wenzelm 2007-01-19 adapted ML context operations;
2006-12-30 wenzelm 2006-12-30 removed conditional combinator;
2006-12-18 haftmann 2006-12-18 switched argument order in *.syntax lifters