Drop rewrite rule arguments of sublocale and interpretation implementations.

Experimental support for rewrite morphisms in locale instances.

provide explicit variant initializers for regular named target vs. almost-named target

tuned signature;

eliminated "xname" and variants;

eliminated unused simproc identifier;

represent both algebraic and local-theory views on locale interpretation in interfaces

--HG--
extra : rebase_source : 0f233aa5dd88ebb1594d03af4f3a3d7b08a44fa7

separate ML module for interpretation

--HG--
extra : rebase_source : 867de135491ddc9e949d932384cce64f60343123

uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
removed obsolete '!' syntax;

simplified simproc programming interfaces;

prefer tactics with explicit context;

clarified context;

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

imitate old "intern" semantics for the sake of outdated/unmaintained code, notably relevant for Simpl;

tuned signature -- prefer qualified names;

proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;

dropped obscure and unused ad-hoc before_exit hook for named targets

removed dead code;

target-sensitive user-level commands interpretation and sublocale

simplifier uses proper Proof.context instead of historic type simpset;

tuned command descriptions;

more method position information, notably finished_pos after end of previous text;

more proof method text position information;

more explicit namespace prefix for 'statespace' -- duplicate facts;

tuned signature;

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

prefer formally checked @{keyword} parser;

locale expressions without source positions;

eliminated some legacy operations;

tuned messages;

misc tuning and modernization;
more antiquotations;

tuned;

uniform Local_Theory.declaration with explicit params;

old term operations are legacy;

simplified/unified Simplifier.mk_solver;

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

more robust exception pattern General.Subscript;

reorganized fixes as specialized (global) name space;

proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way;
tuned;

eliminated old List.nth;
tuned;

modernized structure Proof_Context;

discontinued special treatment of structure Mixfix;
eliminated slightly odd no_syn convenience;

separate structure Term_Position;
dismantled remains of structure Type_Ext;

statespace syntax: strip positions -- type constraints are unexpected here;

added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;

misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;

Add mixins to sublocale command.

turned show_sorts/show_types into proper configuration options;

formerly unnamed infix equality now named HOL.eq

eliminated broken Output.no_warnings_CRITICAL -- context visibility does the job;
modernized attribute setup;

renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;

tuned quotes

use antiquotations for remaining unqualified constants in HOL

Named_Target.init: empty string represents theory target

renamed Theory_Target to the more appropriate Named_Target

--HG--
rename : src/Pure/Isar/theory_target.ML => src/Pure/Isar/named_target.ML

renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;

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

tuned;

farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)

renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;

adapted ProofContext.infer_type;

inline old Record.read_typ/cert_typ;
spelling;

modernized structure Local_Theory;

modernized structure Theory_Target;

adapted Generic_Data, Proof_Data;
tuned;

adapted LocalTheory.declaration;

critical comments;

indicate CRITICAL nature of various setmp combinators;

eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;

replaced String.concat by implode;
replaced String.concatWith by space_implode;
replaced (Seq.flat o Seq.map) by Seq.maps;
replaced List.mapPartial by map_filter;
replaced List.concat by flat;
replaced (flat o map) by maps, which produces less garbage;

Undo errornous commit of Statespace change

correct variable order in approximate-method

modernized messages -- eliminated ctyp/cterm operations;

Method.Basic: no position;

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

unified type Proof.method and pervasive METHOD combinators;

Assumption.all_prems_of, Assumption.all_assms_of;

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

minimal adaptions for abstract binding type;

removed spurious occurrences of old rep_ss;

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

less arbitrary occurrences of undefined

changed locale predicate name convention

locale -> old_locale, new_locale -> locale

locale -> old_locale, new_locale -> locale

--HG--
rename : src/Pure/Isar/locale.ML => src/Pure/Isar/old_locale.ML

avoid implicit use of prems;

adapted statespace module to new locales;

more antiquotations;

cleaned up binding module and related code

adjusted locale signature to *_cmd convention

LocalTheory.exit_global;

fixed headers

explicit type Name.binding for higher-specification elements;

dropped locale (open)

tuned signature;
removed duplicates of read_typ/cert_typ (cf. RecordPackage.read_typ/cert_typ);

tuned signature;
removed duplicate of RecordPackage.read_typ;
replaced Typetab by existing Typtab;

purely functional setup of claset/simpset/clasimpset;

eliminated quiete_mode ref (not really needed);

simplified get_thm(s): back to plain name argument;

renamed datatype thmref to Facts.ref, tuned interfaces;

added ::: / @@@ scanner combinators;

PrintMode.setmp (avoid direct access to print_mode ref);

added signatures;
tuned

added Statespace library