more robust bound_fixes: external name does appear in "fixes" name space and could clash with direct fixes (e.g. via Subgoal.FOCUS within a global context);

tuned signature;

more compact XML: separate environment for free variables;
clarified fold_proof_terms vs. fold_proof_terms_types;

clarified modules;

clarified signature;

more structural integrity;

clarified signature;

tuned signature;

tuned signature;

clarified signature: more types;

eliminated ASCII syntax from Pure bootstrap;
tuned comments;

more symbols;

highlighting of entity def/ref positions wrt. cursor;

back to dummy constraints (amending dd2914250ca7): important for Syntax_Phases.get_free/is_declared;

more accurate mixfix type constraints;

more precise context -- potentially relevant for Eisbach dummy thm;

suppress irrelevant position reports;

clarified context policy to allow multiple dummies;

clarified modules;
tuned signature;

clarified Variable.gen_all;
simplified Local_Defs.export: pointless partial application;

more explicit context;

tuned signature;
clarified context;

SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);

Variable.focus etc.: optional bindings provided by user;
Subgoal.focus command: more careful treatment of user-provided bindings;

simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);

clarified term bindings;

clarified context;

tuned signature;

tuned signature;

tuned signature;

prefer Variable.focus, despite subtle differences of Logic.strip_params vs. Term.strip_all_vars;

tuned;

admit dummy patterns in instantiations;
clarified context;

implicit goal parameters are improper;

added declare_maxidx operations for Eisbach;

clarified Variable.export: observe maxidx of target context;

clarified context;

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

tuned -- more explicit use of context;

tuned signature;

tuned;

renamed "pairself" to "apply2", in accordance to @{apply 2};

tuned signature;

abstract type Name_Space.table;
clarified pretty_locale_deps: sort strings;
clarified Proof_Context.update_cases: Name_Space.del_table hides name space entry as well;

tuned signature;

tuned signature;
tuned message;

general notion of auxiliary bounds within context;
revert_bounds as part of regular unparse_term;
avoid special variants of Syntax.string_of_term in Simplifier (e.g. relevant for add-on tracing);

maintain morphism names for diagnostic purposes;

Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;

tuned;

allow position constraints to coexist with 0 or 1 sort constraints;
more position information in sorting error;
report sorting of all type variables;

report sort assignment of visible type variables;

clarified Binding.name_of vs Name_Space.base_name vs Variable.check_name (see also 9bd8d4addd6e, 3305f573294e);

maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global);
prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output);
simplified signatures;

more direct Name_Space.defined_entry;
tuned Variable.export_inst: avoid keeping full contexts within the gen_fixesT closure (NB: locale infrastructure stores morphisms persistently);

renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;

separate module for concrete Isabelle markup;

--HG--
rename : src/Pure/General/markup.ML => src/Pure/General/isabelle_markup.ML
rename : src/Pure/General/markup.scala => src/Pure/General/isabelle_markup.scala

tuned;

tuned markup -- prefer user-perspective;

discontinued entity text color, notably historic red for classes;
tuned entity names;

tuned;

tuned;

slightly more explicit/syntactic modelling of morphisms;

more thorough Variable.check_name: Binding.check for logical entities within the term language;

tuned signature: Name.invent and Name.invent_names;

simplified Name.variant -- discontinued builtin fold_map;

clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;

tuned signature -- eliminated odd comment;

more informative markup for fixed variables (via name space entry);
uniform markup for undeclared entities;
tuned;

reorganized fixes as specialized (global) name space;

more uniform Variable.add_frees/add_fixed etc.;

modernized structure Proof_Context;

tuned signature, disentangled dependencies;

recovered some odd two-dimensional layout;

modernized structure Ord_List;

load type_infer.ML later -- proper context for Type_Infer.infer_types;
renamed Type_Infer.polymorphicT to Type.mark_polymorphic;

more careful treatment of context visibility flag wrt. spurious warnings;

renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;

simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;

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

renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;

normalized uncurry take/drop

--HG--
extra : rebase_source : 647c8b5a6641f0eef6d4d81646474d16388f9fb9

curried take/drop

--HG--
extra : rebase_source : 6e6b508d936640bef00f0ad0c4fb089ad5253ef0

adapted Generic_Data, Proof_Data;
tuned;

curried inter as canonical list operation (beware of argument order)

dropped redundant gen_ prefix

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

eliminated redundant bindings;

Variable.importT/import: return full instantiations, tuned;

Variable.focus: named parameters;

renamed structure TermSubst to Term_Subst;

renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
renamed Variable.importT_thms to Variable.importT (again);

replaced add_binds by singleton bind_term;

eliminated obsolete var morphism;

Term.declare_typ_names, Term.declare_term_frees;

cleaned up binding module and related code

maintain sort occurrences of declared terms;

added declare_typ;

focus: actually declare constraints for local parameters;

variant_fixes: preserve internal state, mark skolem only for body mode;
import_inst: actually observe is_open flag (cf. variant_fixes);

exported declare_names

refined notion of consts within the local scope;

added is_const/declare_const for local scope of fixes/consts;

add_bind: close_schematic_term;

replaced literal 'a by Name.aT;

maintain maxidx (analogous to name context);
polymorhic: observe Variable.maxidx_of;

declare_constraints: declare (fix) type variables within constraints, but not terms themselves;

added polymorphic_types;

simplified DataFun interfaces;

removed obsolete redeclare_skolems;

Thm.fold_terms;

tuned signature;
export: precomputed closure, no reference to contexts;

renamed Variable.importT to importT_thms;

renamed Variable.import to import_thms (avoid clash with Alice keywords);

tuned expand_binds;

moved hidden_polymorphism to term.ML;

added add_fixed;

added export_morphism;
ProofContext.init;

removed fix_frees interface;
added auto_fixes (depends on body mode);

declare_constraints: reset constraint on dummyS;

tuned Variable.trade;

renamed Variable.invent_fixes to Variable.variant_fixes;

Thm.dest_arg;

moved term subst functions to TermSubst;

normalized Proof.context/method type aliases;
added declare/export/import_prf;
added focus_subgoal: reset/declare goal schematics;

export: refrain from adjusting maxidx;

added add_fixes_direct;
tuned;

added fix_frees (from Isar/proof_context.ML);

import(T): result includes fixed types/terms;
focus: tuned interface;

tuned;

reorganize declarations (more efficient);
renamed rename_wrt to variant_frees (avoid confusion with Term.rename_wrt_term, which reverses the result);
tuned;

added newly_fixed, focus;
removed monomorphic;
tuned;

Name.context already declares empty names;
tune ins_sorts -- sort assigments should never change later;

separate names filed (covers fixes/defaults);

maintain Name.context for fixes/defaults;
more efficient inventing/renaming of local names (cf. name.ML);

polymorphic: always generalize wrt. used_types;

added declare_thm, thm_context;
added trade(T);

major reworking of export functionality -- based on Term/Thm.generalize;
tuned interfaces;

Fixed type/term variables and polymorphic term abbreviations.