src/Pure/Isar/attrib.ML
2010-05-30 wenzelm 2010-05-30 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information; ML_Context.eval/expression expect explicit ML_Lex source, which allows surrounding further text without loosing position information; fall back on ML_Context.eval_text if there is no position or no surrounding text; proper Args.name_source_position for method "tactic" and "raw_tactic"; tuned;
2010-05-17 wenzelm 2010-05-17 renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time; eliminated slightly odd alias structure T;
2010-05-15 wenzelm 2010-05-15 refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;
2010-05-10 wenzelm 2010-05-10 renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
2010-03-28 wenzelm 2010-03-28 pass raw Context.generic, to avoid wasteful Context.proof_of -- Config.get_thy is often used in performance critical spots like unify.ML;
2010-03-28 wenzelm 2010-03-28 configuration options admit dynamic default values;
2010-03-28 wenzelm 2010-03-28 do not export Attrib.register_config, to make it harder to use low-level Config.declare after the bootstrap phase;
2010-03-26 boehmes 2010-03-26 replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-03-07 wenzelm 2010-03-07 modernized structure Local_Defs;
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2010-01-30 berghofe 2010-01-30 Added "constraints" tag / attribute for specifying the number of equality constraints in cases rules.
2009-11-13 wenzelm 2009-11-13 eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-11-01 wenzelm 2009-11-01 modernized structure Rule_Cases;
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-06-24 wenzelm 2009-06-24 renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported); renamed Variable.importT_thms to Variable.importT (again);
2009-06-02 wenzelm 2009-06-02 merged, resolving conflict in src/Pure/Isar/attrib.ML;
2009-06-02 haftmann 2009-06-02 made SML/NJ happy
2009-06-01 wenzelm 2009-06-01 made SML/NJ happy;
2009-05-30 wenzelm 2009-05-30 eliminated old Attrib.add_attributes (and Attrib.syntax);
2009-05-30 wenzelm 2009-05-30 modernized attribute setup; removed obsolete no_args, add_del_args;
2009-05-18 haftmann 2009-05-18 introduced Thm.generatedK
2009-05-16 bulwahn 2009-05-16 added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
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 added map_facts_refs;
2009-03-18 wenzelm 2009-03-18 more precise type Symbol_Pos.text;
2009-03-16 wenzelm 2009-03-16 tuned signature;
2009-03-15 wenzelm 2009-03-15 added setup and attribute_setup -- expect plain parser instead of syntax function; aded add_del parser;
2009-03-13 wenzelm 2009-03-13 eliminated type Args.T; pervasive types 'a parser and 'a context_parser;
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-03 wenzelm 2009-03-03 Thm.binding;
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-01-29 berghofe 2009-01-29 Added abs_def attribute.
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2008-12-05 haftmann 2008-12-05 removed Table.extend, NameSpace.extend_table
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
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-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-08-10 wenzelm 2008-08-10 pass position to get_fact; tuned;
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token, renamed some operations; unified version of thm_sel (formerly in args.ML and spec_parse.ML);
2008-08-06 wenzelm 2008-08-06 report markup;
2008-08-04 wenzelm 2008-08-04 tuned signature; eliminated obsolete pervasives;
2008-05-14 wenzelm 2008-05-14 added defined;
2008-04-17 wenzelm 2008-04-17 no_vars: reset body mode, i.e. invent global frees (which are acceptable to Variable.auto_fixes);
2008-04-16 wenzelm 2008-04-16 PureThy.get_fact: pass dynamic context;
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2008-03-20 wenzelm 2008-03-20 Facts.Named: include position;
2008-03-20 wenzelm 2008-03-20 renamed former get_thms(_silent) to get_fact(_silent);
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2008-01-26 wenzelm 2008-01-26 misc tuning and internal rearrangement; tuned attribute syntax -- no need for eta-expansion;
2007-09-26 wenzelm 2007-09-26 added eval_thms;
2007-09-25 wenzelm 2007-09-25 tuned functor application;