unused;

tuned signature: eliminated pointless type Context.pretty;

subtle change of long-standing name space policy: unknown entries are treated as hidden, consequently "private" is understood in the strict sense;

tuned signature;

tuned signature;

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

clarified name of Type.unified, to emphasize its connection to the "unify" family;
tuned low-level operation;

recovered type matching, which was broken in 8a765db7e0f8 (see also 8a765db7e0f8, 2db1d3d2ed54);
NB: "match" operates on direct substitution without variable chasing, in contrast to "unify" (and Unify.matches!) which work on cascaded env;

more frugal recording of changes: join merely requires information from one side;
tuned;

more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;

minor performance tuning via fast matching filter;

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;

unused;

reject internal term names outright, and complete consts instead;
more general Name_Space.check_reports;
more compact Markup.markup_report;

more markup for inner syntax class/type names (notably for completion);
explicit reports result without broadcast yet, which is important for brute-force disambiguation;

prefer Name_Space.check with its builtin reports (including completion);

prefer explicitly qualified exceptions, which is particular important for robust handlers;

tuned exceptions -- avoid composing error messages in low-level situations;

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

use explicit Type.strip_sorts_dummy to suppress sort constraints in output;

renamed Position.str_of to Position.here;

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;

clarifed name space "type name", which covers logical and non-logical types, and often occurs inside outer syntax "type" markup;

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

clarified certify vs. sharing;

pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;

avoid OldTerm operations -- with subtle changes of semantics;

entity markup for "type", "constant";

type classes: entity markup instead of old-style token markup;

simplified Name.variant -- discontinued builtin fold_map;

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

clarified Type.the_decl;

pass plain Proof.context for pretty printing;

simplified Sorts.class_error: plain Proof.context;
tuned;

simplified pretty printing context, which is only required for certain kernel operations;
disentangled dependencies of structure Pretty;

added Binding.print convenience, which includes quote already;

report Name_Space.declare/define, relatively to context;
added "global" variants of context-dependent declarations;

Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;

uniform treatment of typ_match and raw_match (cf. b654fa27fbc4);

extra checking of name bindings for classes, types, consts;
tuned;

prevention of self-referential type environments

Type_Infer.preterm: eliminated separate Constraint;

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

common Type.appl_error, which also covers explicit constraints;

eliminated aliases of Type.constraint;

proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
* present type variables are only compared wrt. first component (the atomic type), not the duplicated sort;
* extra sorts are grounded towards fixed 'a, potentially with different sorts (the original version with Name.names could cause name clashes with other present variables, too, but this should not be a problem);
* deriv_rule_unconditional ensures that proof terms are always maintained independently of the "proofs" flag -- this improves robustness and preserves basic PThm proofs required for extraction attributes, e.g. in theory HOL/Extraction;

more systematic naming of tsig operations;

export Type.minimize_sort;

renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;

aliases for class/type/const;
tuned;

added ProofContext.tsig_of -- proforma version for local name space only, not logical content;
added ProofContext.read_type_name_proper;
localized ProofContext.read_class/read_arity/cert_arity;
localized ProofContext.class_space/type_space etc.;

provide direct access to the different kinds of type declarations;

avoid exporting Type.build_tsig

exported build_tsig

explicitly mark some legacy freeze operations;

locale_const/target_notation: uniform use of Term.aconv_untyped;
target_notation: pass on transformed term formally;
removed obsolete Type.similar_types;

adapted Generic_Data, Proof_Data;
tuned;

eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;

maintain position of formal entities via name space;

maintain explicit name space kind;
export Name_Space.the_entry;
tuned messages;

renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;

eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
simplified messages;

eliminated redundant bindings;

explicit indication of Unsynchronized.ref;

Correct chasing of type variable instantiations during type unification.
The following theory should not raise exception TERM:

constdefs
somepredicate :: "(('b => 'b) => ('a => 'a))
=> 'a => 'b => bool"
"somepredicate upd v x == True"

lemma somepredicate_idI:
"somepredicate id (f v) v"
by (simp add: somepredicate_def)

lemma somepredicate_triv:
"somepredicate upd v x ==> somepredicate upd v x"
by assumption

lemmas somepredicate_triv [OF somepredicate_idI]

lemmas st' = somepredicate_triv[where v="h :: nat => bool"]

lemmas st2 = st'[OF somepredicate_idI]

eq_type: special case for empty environment;

witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables;

replace old bstring by binding for logical primitives: class, type, const etc.;

moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
use regular Term.add_XXX etc.;

moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
tuned signature of structure Term;

varify: regular name context;

dropped NameSpace.declare_base

cleaned up binding module and related code

type Properties.T;

the_tags: explicit error message;
new_decl: Position.thread_data;

type constructors now with markup

add_abbrev: check tfrees of rhs, not tvars (addresses a lapse introduced in 1.65);

simplified hide_XXX interfaces;

tsig: removed unnecessary universal witness;
Sorts.class_error: produce message only (formerly msg_class_error);

canonical meet_sort operation

Type.lookup now curried; typ_of_sort

similar_types: uniform treatment of TFrees/TVars;

tuned signature;

replaced Term.equiv_types by Type.similar_types;

replaced literal 'a by Name.aT;

maintain mode in context (get/set/restore_mode);

type mode: models certification mode (default, syntax, abbrev);
replaced certify_typ_syntax/abbrev by certify_typ_mode;

replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;

simplified/unified list fold;

Sorts.minimal_classes;

avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;

fixed type signature of Type.varify

gen_rem(s) abandoned in favour of remove / subtract

serial numbers for types;

renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);

replaced Term.variant(list) by Name.variant(_list);

renamed Type.(un)varifyT to Logic.(un)varifyT;
made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround;

export raw_unifys, could_unifys;

export raw_matches;

more abstract interface to classes/arities;

replaced Sorts.DOMAIN by general Sorts.CLASS_ERROR;
add_types etc.: reject qualified dummy types -- prevents users from messing up some internal conventions;

tuned;

build classes/arities: refer to operations in sorts.ML;
simplified add_class/classrel/arity;
tuned;

added inter_sort;
added arity_number/sorts;

avoid polymorphic equality;

got rid of type Sign.sg;

renamed gen_duplicates to duplicates;

TableFun: renamed xxx_multi to xxx_list;
tuned;

subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate

added could_unify;

minor tweaks for Poplog/ML;

slight adaptions to library changes

TableFun/Symtab: curried lookup and update;

curried_lookup/update;

use AList operations;

typ_match, unify: canonical argument order;
added raw_match, raw_instance;
proper implementation of raw_unify;

tuned match, unify;

Moved eq_type from envir.ML to type.ML

Symtab.fold;

name space of classes and types maintained in tsig;

renamed cert_typ_raw to cert_typ_abbrev;
renamed add_abbrs to add_abbrevs;
tuned;

added Type.freeze(_type);
tuned;

- Eliminated nodup_vars check.
- Unification and matching functions now check types of term variables / sorts
of type variables when applying a substitution.
- Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list
as argument, to allow for proper instantiation of theorems containing
type variables with same name but different sorts.

Removed practically all references to Library.foldr.

Move towards standard functions.

Deleted Library.option type.

tuned;

tuned certify_typ/term;

tuned certify_typ;

tuned messages;

removed norm_typ; improved output; refer to Pretty.pp;

major cleanup of tsig datastructures and extend/merge operations; fixes old bugs in classes/arities code; proper treatment of nonterminals and syntax-only types;

Removed add_env because Vartab.map was too slow for large environments.

paramify_dummies: proper treatment of maxidx;

tuned interface of unify, param;
added paramify_dummies to turn TypeInfer.anyT into unifiable parameter;

varify returns newly introduced variables;

Syntax.typ_of_term: pass intern sort fn;

ext_tsig_classes: rebuild_tsig!!!!!

ext_classrel: certify_class;

export freeze_thaw_type;

typ_no_norm;

removed is_type_abbr;

NameSpace.is_qualified;

added is_type_abbr;

tuned;

Type.unify and Type.typ_match now use Vartab instead of association lists.

added witness_sorts, univ_witness;
removed nonempty_sort;
tsig: log_types, univ_witness (require rebuild_tsig!);
heavily tuned;

freeze_thaw does nothing if no variables

replaced assoc lists by Symtab.table;

fixed param;

defaults for free variables hide consts of same name;

fixed error msgs;

added param;

fixed exception OPTION;

decode: qualified is always const;

tuned decode;

eliminated raise_term, raise_typ;
tuned get_sort, decode_types, infer_types to accomodate qualified names;

Removal of freeze_vars and thaw_vars. New freeze_thaw

of_sort: type_sig -> typ * sort -> bool;

tuned check_has_sort;
fixed norm_typ: also does norm_sort;

improved type check error messages;

moved classes / sorts to sorts.ML;
moved (and reimplemented) type inference to type_infer.ML;
cleaned up type unification;
misc cleanup and tuning;

Removed some polymorphic equality tests

Replaced "flat" by the Basis Library function List.concat

Added optimization: do nothing for empty list

fixed comment;

added eq_sort (will move to sorts.ML eventually);
added get_sort (handles constraints / defaults);
attach_types: adapted to new get_sort;

Tidying and renaming of function Dom

Removed or eta-expanded some declarations that are illegal under value
polymorphism

Removal of polymorphic equality via mem, subset, eq_set, etc

maxidx_of_typs replaces max o map maxidx_of_typ

Optimized type inference (avoids chains of
the form 'a |-> 'b |-> 'c ... in tye)

Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.

renamed expand_typ to norm_typ

inserted tabs again

removed tabs

Removed bug in type unification. Negative indexes are not used any longer.
Had to change interface to Type.unify to pass maxidx. Thus changes in the
clients.

infer_types now takes a term list and a type list as argument. It
is defined using the new function infer_terms. Error messages and
comments also improved.

added comment;

nonempty_sort: no longer var names as args;

added nonempty_sort (a somewhat braindead version!);

Corrected a silly old bug in merge_tsigs.
Rewrote a lot of Nimmermann's code.

Changed treatment of during type inference internally generated type
variables.

1. They are renamed to 'a, 'b, 'c etc away from a given set of used names.
2. They are either frozen (turned into TFrees) or left schematic (TVars)
depending on a parameter. In goals they are frozen, for instantiations they
are left schematic.

improved expand_typ (now handles TVars);
slightly changed ext_tsig_abbrs;
added ext_tsig_arities;
removed extend_tsig;
various internal changes;

Pure/type/unvarifyT: moved there from logic.ML

added ext_tsig_types;
various minor changes;

slightly changed args of infer_types;
replaced parents by enclose;
renamed 2nd add_types to attach_types and fixed the
typevar-sort-constraint BUG;
various minor internal changes;

added raw_unify;

added ext_tsig_subclass, ext_tsig_defsort;
minor internal rearrangements;

restored functor sig;
added str_of_sort, str_of_arity, rem_sorts;
minor internal cleanup;

replaced "logic" by logicC;
added subsort, norm_sort;

(this is a preliminary release)
type abbreviations;

Necessary changes to accomodate type abbreviations.

added rep_tsig

added logical_types

Initial revision