Syntax.read_typ; rule_tac etc.: proper read_termTs (discontinued rogue type-inference);

export read_const'; tuned;

Syntax.read_typ;

added inductive

attribute where/of: proper Syntax.parse/check;

discontinued ProofContext.read_prop_legacy; removed obsolete Sign.read_tyname/const (cf. ProofContext); refined notion of consts within the local scope;

discontinued ProofContext.read_prop_legacy;

refined Variable.declare_const; removed obsolete Sign.read_tyname/const (cf. ProofContext);

refined notion of consts within the local scope;

tuned signature;

removed obsolete Sign.read_tyname/const (cf. ProofContext);

map and prefix

activated HOL-SizeChange; tuned;

tuned;

read_const/legacy_intern_skolem: cover consts within the local scope;

synchronize_syntax: declare operations within the local scope of fixes/consts (still inactive -- breaks rogue type-inference of rule_tac/where/of);

fixed spelling; tuned;

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

removed dependencies on Size_Change_Termination from HOL-Library;

moved stuff about size change termination to its own session

clarifying comment

clarified merge

Class.init now similiar to Locale.init

CRITICAL force