src/Pure/Isar/attrib.ML
2011-11-17 wenzelm 2011-11-17 partial evaluation in invisible context;
2011-11-16 wenzelm 2011-11-16 retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;
2011-11-16 wenzelm 2011-11-16 clarified Attrib.partial_evaluation;
2011-11-14 wenzelm 2011-11-14 some support for partial evaluation of attributed facts;
2011-11-14 wenzelm 2011-11-14 eliminated dead code;
2011-11-07 wenzelm 2011-11-07 tuned signature -- avoid spurious Thm.mixed_attribute;
2011-11-06 wenzelm 2011-11-06 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute; misc tuning;
2011-08-06 kleing 2011-08-06 make syntax ambiguity warnings a config option
2011-08-08 wenzelm 2011-08-08 made SML/NJ happy;
2011-08-06 nipkow 2011-08-06 extended user-level attribute case_names with names for case hypotheses
2011-06-10 wenzelm 2011-06-10 tuned name (cf. blast_stats);
2011-05-15 wenzelm 2011-05-15 optional description for 'attribute_setup' and 'method_setup';
2011-05-14 wenzelm 2011-05-14 discontinued global config options within attribute name space;
2011-05-03 wenzelm 2011-05-03 more conventional naming scheme: names_long, names_short, names_unique;
2011-05-02 wenzelm 2011-05-02 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings;
2011-04-17 wenzelm 2011-04-17 markup attributes/methods via name space; eliminated obsolete markup;
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-16 wenzelm 2011-04-16 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-04-08 wenzelm 2011-04-08 discontinued special status of structure Printer;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-04-07 wenzelm 2011-04-07 tuned signature;
2011-04-05 wenzelm 2011-04-05 discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
2011-03-22 wenzelm 2011-03-22 enable inner syntax source positions by default (controlled via configuration option); disable source positions for HOLCF, due to special pattern translations;
2010-12-21 wenzelm 2010-12-21 configuration option "syntax_ast_trace" and "syntax_ast_stat";
2010-12-21 wenzelm 2010-12-21 configuration option "ML_trace";
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-12-16 boehmes 2010-12-16 turned simp_trace_depth_limit into a configuration option
2010-12-02 wenzelm 2010-12-02 configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
2010-12-02 wenzelm 2010-12-02 renamed trace_simp to simp_trace, and debug_simp to simp_debug;
2010-10-30 wenzelm 2010-10-30 support for real valued configuration options;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-17 wenzelm 2010-09-17 tuned signature of (Context_)Position.report variants;
2010-09-06 wenzelm 2010-09-06 turned show_hyps and show_tags into proper configuration option;
2010-09-06 wenzelm 2010-09-06 more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
2010-09-05 wenzelm 2010-09-05 turned show_brackets into proper configuration option; Sign.certify/type_check: dropped Syntax.pp_show_brackets, which is hard to hold up due to Pretty.pp and not even present in the regular end-user type check;
2010-09-05 wenzelm 2010-09-05 turned show_sorts/show_types into proper configuration options;
2010-09-03 wenzelm 2010-09-03 turned eta_contract into proper configuration option;
2010-09-03 wenzelm 2010-09-03 turned show_structs into proper configuration option;
2010-09-03 wenzelm 2010-09-03 configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
2010-09-03 wenzelm 2010-09-03 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
2010-09-03 wenzelm 2010-09-03 treat show_free_types as plain ML option, without the extras of global default and registration in the attribute name space -- NB: 'print_configs' only shows the latter;
2010-09-03 wenzelm 2010-09-03 more explicit Config.declare vs. Config.declare_global;
2010-09-03 wenzelm 2010-09-03 turned show_no_free_types into proper configuration option show_free_types, with flipped polarity;
2010-09-03 wenzelm 2010-09-03 turned show_consts into proper configuration option;
2010-09-02 wenzelm 2010-09-02 turned show_question_marks into proper configuration option; show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname; tuned;
2010-08-11 wenzelm 2010-08-11 tuned eval_thms (cf. note etc. in proof.ML);
2010-08-11 wenzelm 2010-08-11 use Pretty.enum convenience;
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.