clarified modules;

isabelle update -u control_cartouches;

clarified take/drop/chop prefix/suffix;

clarified syntax;

support 'assumes' in specifications, e.g. 'definition', 'inductive';
tuned signatures;

more general types Proof.method / context_tactic;
proper context for Method.insert_tac;
tuned;

updated to infer_instantiate;

renamed ML funs

tuned signature;

@{command_spec} is superseded by @{command_keyword};

Thm.cterm_of and Thm.ctyp_of operate on local context;

tuned signature -- prefer qualified names;

eliminated some clones of Proof_Context.cterm_of

proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);

renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place

--HG--
rename : src/HOL/Datatype.thy => src/HOL/Old_Datatype.thy
rename : src/HOL/Tools/Function/size.ML => src/HOL/Tools/Function/old_size.ML
rename : src/HOL/Tools/Datatype/datatype.ML => src/HOL/Tools/Old_Datatype/old_datatype.ML
rename : src/HOL/Tools/Datatype/datatype_aux.ML => src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
rename : src/HOL/Tools/Datatype/datatype_codegen.ML => src/HOL/Tools/Old_Datatype/old_datatype_codegen.ML
rename : src/HOL/Tools/Datatype/datatype_data.ML => src/HOL/Tools/Old_Datatype/old_datatype_data.ML
rename : src/HOL/Tools/Datatype/datatype_prop.ML => src/HOL/Tools/Old_Datatype/old_datatype_prop.ML
rename : src/HOL/Tools/Datatype/datatype_realizer.ML => src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML
rename : src/HOL/Tools/Datatype/primrec.ML => src/HOL/Tools/Old_Datatype/old_primrec.ML
rename : src/HOL/Tools/Datatype/rep_datatype.ML => src/HOL/Tools/Old_Datatype/old_rep_datatype.ML

simplified type Proof.method;

more qualified names;

proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;

outer syntax command definitions based on formal command_spec derived from theory header declarations;

prefer formally checked @{keyword} parser;

discontinued old-style Term.list_all_free in favour of plain Logic.all;

more antiquotations;

do not open ML structures;

added ML antiquotation @{attributes};

modernized signature of Term.absfree/absdummy;
eliminated obsolete Term.list_abs_free;

old term operations are legacy;

simplified Name.variant -- discontinued builtin fold_map;

discontinued Name.variant to emphasize that this is old-style / indirect;

modernized structure Proof_Context;

standardized split_last/last_elem towards List.last;
eliminated obsolete Library.last_elem;

prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
eliminated old-style structure aliases K = Keyword, P = Parse;

prefer structure Parse_Spec;

modernized naming conventions of main Isar proof elements;

Fixed bug in code for guessing the name of the variable representing the freshness context.

modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML

--HG--
rename : src/HOL/Tools/Datatype/datatype.ML => src/HOL/Tools/Datatype/datatype_data.ML
extra : rebase_source : 552900fbf6783258465fa5000202d52cf1f99a1f

adapted Local_Theory.define -- eliminated odd thm kind;

eliminated slightly odd name space grouping -- now managed by Isar toplevel;

modernized structure Local_Theory;

eliminated slightly odd kind argument of LocalTheory.note(s);
added LocalTheory.notes_kind as fall-back for unusual cases;

eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);

standardized filter/filter_out;

name space groups are identified by serial, not serial_string;

renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"

removed old-style \ and \\ infixes

dropped redundant gen_ prefix

replaced old_style infixes eq_set, subset, union, inter and variants by generic versions

fixed Method.Basic;

Method.Basic: no position;

nominal.ML is nominal_datatype.ML

renamed NamedThmsFun to Named_Thms;
simplified/unified names of instances of Named_Thms;

discontinued ancient tradition to suffix certain ML module names with "_package"

--HG--
rename : src/HOL/Import/import_package.ML => src/HOL/Import/import.ML
rename : src/HOL/Nominal/nominal_package.ML => src/HOL/Nominal/nominal.ML
rename : src/HOL/Tools/specification_package.ML => src/HOL/Tools/choice_specification.ML
rename : src/HOL/Tools/datatype_package/datatype_package.ML => src/HOL/Tools/datatype_package/datatype.ML
rename : src/HOL/Tools/function_package/fundef_package.ML => src/HOL/Tools/function_package/fundef.ML
rename : src/HOL/Tools/inductive_package.ML => src/HOL/Tools/inductive.ML
rename : src/HOL/Tools/inductive_set_package.ML => src/HOL/Tools/inductive_set.ML
rename : src/HOL/Tools/old_primrec_package.ML => src/HOL/Tools/old_primrec.ML
rename : src/HOL/Tools/primrec_package.ML => src/HOL/Tools/primrec.ML
rename : src/HOL/Tools/recdef_package.ML => src/HOL/Tools/recdef.ML
rename : src/HOL/Tools/record_package.ML => src/HOL/Tools/record.ML
rename : src/HOL/Tools/typecopy_package.ML => src/HOL/Tools/typecopy.ML
rename : src/HOL/Tools/typedef_package.ML => src/HOL/Tools/typedef.ML

introduced Thm.generatedK

added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages

unified type Proof.method and pervasive METHOD combinators;

simplified preparation and outer parsing of specification;
export extern cmd interfaces as well;

moved basic algebra of long names from structure NameSpace to Long_Name;

renamed NameSpace.base to NameSpace.base_name;
renamed NameSpace.map_base to NameSpace.map_base_name;
eliminated alias Sign.base_name = NameSpace.base_name;

Fix parentheses.

Added "nitpick_const_simp" attribute to Nominal primrec.

Merge.

renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
minor tuning;

binding is alias for Binding.T

qualified Term.rename_wrt_term;

moved old add_term_vars, add_term_frees etc. to structure OldTerm;

Modified nominal_primrec to make it work with local theories, unified syntax
with the one used by fun(ction) and new version of primrec command.

Name.name_of -> Binding.base_name

cleaned up binding module and related code

arbitrary is undefined

explicit type Name.binding for higher-specification elements;

PureThy: dropped note_thmss_qualified, dropped _i suffix

moved global pretty/string_of functions from Sign to Syntax;

eliminated quiete_mode ref (unused);

added new primrec package

turned keywords invariant/freshness_context into reserved indentifiers;

simplified interfaces for outer syntax;

proper Sign operations instead of Theory aliases;

Syntax.parse/check/read;

replaced ProofContext.infer_types by general Syntax.check_terms;

Moved unify_consts to PrimrecPackage.

balanced conjunctions;

Method.Basic: include position;

Fixed bug in subst causing primrec functions returning functions
to be rejected.

simplified ProofContext.infer_types(_pats);

removed obsolete TypeInfer.logicT -- use dummyT;

proper ProofContext.infer_types;

- Replaced fold by fold_rev to make sure that list of predicate
variables pvars (for invariants) is in the correct order
- Adapted to new format of datatype descriptor

Replaced "raise RecError" by "primrec_err" in function
gen_primrec_i to prevent error message from being suppressed.

moved parts of OuterParse to SpecParse;

nominal_primrec now prints initial proof state.

Added missing "standard"

Implemented new "nominal_primrec" command for defining
functions on nominal datatypes.