clarified signature: store full theory name;

clarified signature;

support for a soft-type system within the Isabelle logical framework;

unused;

tuned signature: eliminated pointless type Context.pretty;

clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);

support for 'restricted' modifier: only qualified accesses outside the local scope;

support private scope for individual local theory commands;
tuned signature;

tuned signature;

support for explicit scope of private entries;

clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;

tuned signature;

tuned signature;

tuned signature;

more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges;
clarified sublocale_global: proper Local_Theory.exit (see also 8fe7414f00b1);

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;

tuned signature -- prefer Name_Space.get with its builtin error;

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;

syntax translations always depend on context;

comment;

tuned;

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;

prefer Parser.make_gram over Parser.merge_gram, to approximate n-ary merges on theory import;
prefer non-strict lazy over strict future;

sort assignment before simultaneous term_check, not isolated parse_term;
prefer Syntax.read_typ over Syntax.parse_typ, to include check phase for sort assignment;
simplified Syntax_Phases.decode_sort/decode_typ;
discontinued unused Proof_Context.check_tvar;

sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML);
minor tuning;

more robust exception pattern General.Subscript;

standardized aliases of operations on tsig;

pass plain Proof.context for pretty printing;

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;

eliminated obsolete markup -- superseded by generic "entity" markup;

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

modernized structure Proof_Context;

prefer local name spaces;
tuned signatures;
tuned;

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

simplified Pure syntax bootstrap;

discontinued special treatment of structure Lexicon;

discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
clarified Syntax.root;

--HG--
rename : src/Pure/Syntax/syn_ext.ML => src/Pure/Syntax/syntax_ext.ML

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

explicit structure Syntax_Trans;
discontinued old-style constrainAbsC;

--HG--
rename : src/Pure/Syntax/syn_trans.ML => src/Pure/Syntax/syntax_trans.ML

discontinued user-defined token translations;
tuned signature;

typed_print_translation: discontinued show_sorts argument;

discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;

added Position.reports convenience;
modernized Syntax.trrule constructors;
modernized Sign.add_trrules/del_trrules: internal arguments;
modernized Isar_Cmd.translations/no_translations: external arguments;
explicit syntax categories class_name/type_name, with reports via type_context;
eliminated former class_name/type_name ast translations;
tuned signatures;

added Syntax.default_root;
simplified Syntax.parse operations;
clarified treatment of syntax root for translation rules -- refrain from logical_type replacement;
tuned error message;

tuned signature of (Context_)Position.report variants;

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;

turned show_brackets into proper configuration option;
Sign.certify/type_check: dropped Syntax.pp_show_brackets, which is hard to hold up due to Pretty.pp and not even present in the regular end-user type check;

pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;

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

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

more systematic naming of tsig operations;

modernized/simplified Sign.set_defsort;

replaced old Sign.add_tyabbrs(_i) by Sign.add_type_abbrev (without mixfix);
misc tuning and simplification;

misc tuning and simplification;

disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
eliminated obsolete Sign.cert_def;
misc tuning and clarification;

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

tuned;

moved old Sign.intern_term to the place where it is still used;

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.;

authentic syntax for classes and type constructors;
read/intern formal entities just after raw parsing, extern just before final pretty printing;
discontinued _class token translation;
moved Local_Syntax.extern_term to Syntax/printer.ML;
misc tuning;

more uniform treatment of syntax for types vs. consts;

read_class: perform actual read, with source position;

provide direct access to the different kinds of type declarations;

slightly more abstract syntax mark/unmark operations;

authentic syntax for *all* term constants;

more systematic treatment of qualified names derived from binding;

discontinued unnamed infix syntax;

discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);

dropped copy operation for legacy TheoryDataFun

uniform new_group/reset_group;
tuned signature;

modernized structure Primitive_Defs;

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

maintain theory name via name space, not tags;
AxClass.thynames_of_arity: explicit theory name, not tags;

more direct access to naming;
tuned signature;

allow name space entries to be "concealed" -- via binding/naming/local_theory;

maintain position of formal entities via name space;

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

removed redundant Sign.certify_prop, use Sign.cert_prop instead;
tuned;

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

use Name.of_binding for basic logical entities without name space (fixes, case names etc.);

removed obsolete no_base_names naming policy;

renamed sticky_prefix to mandatory_path;

eliminated qualified_names naming policy: qualified names are only permitted via explicit Binding.qualify/qualified_name etc. (NB: user-level outer syntax should never do this);

removed obsolete absolute_path -- use root_path with qualified binding;

explicit root_path, parent_path;
derived absolute_path;
tuned;

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

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

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

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.str_of;

eliminated NJ's List.nth;

removed Ids;

binding is alias for Binding.T

Name.name_of -> Binding.base_name

cleaned up binding module and related code

new Binding module

dropped legacy naming code

using name bindings

namify and name_decl combinators

declare_const: Name.binding, store/report position;

type Properties.T;

type constructors now with markup

moved get_sort to Isar/proof_context.ML;
removed obsolete read_def_typ, read_typ, read_typ_syntax, read_typ_abbrev;

removed obsolete term reading operations (cf. old_goals.ML for legacy emulations);

certify_term: reject qualified frees;

map_const: soft version, no failure here;

add constants: set Markup.theory_nameN in tags;

moved global pretty/string_of functions from Sign to Syntax;

added pretty_global flag;

token translations: context dependent, result Pretty.T;

removed obsolete SIGN_THEORY -- no name aliases in structure Theory;
simplified hide_XXX interfaces;
moved hide_names to isar_cmd.ML;

tsig: removed unnecessary universal witness;

rep_cterm/rep_thm: no longer dereference theory_ref;
removed obsolete compression;

added mk_const functions

standard_parse_term: check ambiguous results without changing the result yet;

separated typedecl module, providing typedecl command with interpretation

syntax operations: turned extend'' into update'' (absorb duplicates);

notation: based on Syntax.update_const_gram (avoids duplicates);

tyabbr/syntax/consts: replaced obsolete read_typ by Syntax.parse_typ/certify_typ;

removed unused read_def_terms';

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

no_variables: tuned error msg;

removed unused set_policy;

add_abbrev: removed Logic.legacy_varifyT, do not unvarify result (again);
added revert_abbrev;

renamed Consts.the_declaration to Consts.the_type;

add_abbrevs: unvarify result;

dest/cert_def: replaced Pretty.pp by explicit Proof.context;

tuned;

replaced Sign.add_consts_authentic by Sign.declare_const;

generalized notation interface (add or del);

generic Syntax.pretty/string_of operations;
existing pretty_term = Syntax.pretty_term o ProofContext.init etc.;
removed pretty_classrel/arity (cf. Syntax/syntax.ML);

add_consts_authentic/add_abbrev: tags (Markup.property list);
tuned signature;

removed obsolete external interface add_const_constraint;
removed redundant const_constraint;
renamed add_const_constraint_i to add_const_constraint;

added minimize_sort, complete_sort;

Syntax.parse/check/read;

certify': proper do_expand argument (which observes force_expand consts) instead of home-grown normalize;

read_def_terms: replaced full Syntax.check_typs by certify_typ, to workaround problems with illegal schematic type vars;

infer_types: general check_typs instead of Type.cert_typ_mode;

read_def_terms: moved disambig to syntax.ML;

replaced certify_typ_syntax/abbrev by certify_typ_mode;
removed obsolete read_sort', read_typ', read_typ_syntax', read_typ_abbrev';

PrimitiveDefs.dest_def;
Syntax.standard_read;

read_def_terms': restrict scope of disambiguation to individual term;

certify: no check_thy here;

moved exception capture/release to structure Exn;

type output = string indicates raw system output;

simplified pretty token metric: type int;

simplified DataFun interfaces;

renamed some old names Theory.xxx to Sign.xxx;

renamed some old names Theory.xxx to Sign.xxx;

export get_sort (belongs to Syntax module);

removed obsolete TypeInfer.logicT -- use dummyT;

removed obsolete infer_types(_simult);
read_sort/get_sort, read_def_terms: internal reorganization;

read_typ_XXX: no sorts;
added read_def_typ (formerly read_typ);

moved ML translation interfaces to isar_cmd.ML;

adapted ML context operations;

replaced classes by all_classes (topologically sorted);
added minimal_classes;

add_abbrev: tuned signature;

advanced translation functions: Proof.context;

added no_frees;
add_abbrev: tuned handling of frees, temp workaround;

tuned Consts signature;

simplified add_abbrev -- single argument;

simplified add_abbrevs: no mixfix;

add_abbrevs: moved common parts to consts.ML;

add_notation: permissive about undeclared consts;

abbrevs: return result;

replaced const_syntax by notation, which operates on terms;

added const_syntax_name;

Syntax.mode;

consts: syntax consts only for actual syntax;

member (op =);

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

tuned;

read_def_cterms (legacy version): Consts.certify;

moved pprint functions to Isar/proof_display.ML;

Sign.infer_types: Name.context;

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

consts: replaced early'' flag by inverted authentic'';
tuned interfaces;

always preserve authentic consts -- removed Syntax.mixfix_const;

added add_const_syntax, add_consts_authentic;
tuned interface;

more abstract interface to classes/arities;

removed add_classes/classrel/arities (superceded by AxClass.axiomatize_class/classrel/arity);
added primitive_class/classrel/arity;

tuned basic list operators (flat, maps, map_filter);

added arity_number/sorts;
tuned;

added typ_equiv;
read_class: improved error;

added super_classes (from sorts.ML);
removed read/cert_classrel (see axclass.ML);

Term.itselfT;

abbrevs: mode does not affect name space;

pretty_term': early vs. late externing (support authentic syntax);
add_abbrevs(_i): support print mode and authentic syntax;

export arities_of instead of classes_arities_of;

declared_const: check for type constraint only, i.e. admit abbreviations as well;
added del_trrules(_i);

got rid of type Sign.sg;

added read_class, read/cert_classrel/arity (from axclass.ML);

add_const_constraint(_i): demand TFrees instead of TVars, optional type (i.e. may delete constraints);

replaced qualified_force_prefix to sticky_prefix;

removed custom_accesses;
added qualified_force_prefix;

tuned extern_term, pretty_term';

export consts_of;
removed const_expansion;
pretty_term', infer_types(_simult): separate Consts.T argument;
added generic certify;
simplified certify_term/prop;

added add_abbrevs(_i);
moved const_of_class/class_of_const to logic.ML;
added no_vars (from theory.ML);
added cert_def;
added const_expansion;
certify: refer to Consts.certify, which includes expansion;

subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate

added specific map_typ/term (from term.ML);

advanced translations: Context.generic;

Syntax.basic_syn;

sane ERROR handling;

tuned;

added const_instance;

uncurried Consts.typargs;

moved consts declarations to consts.ML;

certify_term: tuned monomorphic consts;

consts: monomorphic;

slight adaptions to library changes

TableFun/Symtab: curried lookup and update;

extend: NameSpace.default_naming;

added hide_names(_i) (from isar_thy.ML);

curried_lookup/update;

tuned classes_arities_of;

use AList operations;

added interfaces for compile translation functions (from Isar/isar_thy.ML);

added selectors 'classes_of' and 'classes_arities_of'

added 'the_const_constraint'

Compress.typ;

added add_const_constraint(_i), const_constraint;
added typ_match, typ_unify;

Inttab.defined;

Context.check_thy;

added all_sorts_nonempty;

eliminated separate syn type -- advanced trfuns already part of Syntax.syntax;

renamed init to init_data;

added certify_prop, cert_term, cert_prop;

obsolete type sg is now an alias for Context.theory;
code and interfaces related to stamps and data now in context.ML;
actual signature content declared as theory data;
removed type sg_ref (superceded by theory_ref);
signature SIGN_THEORY lists theory operations that are duplicated in Theory;

discontinued named name spaces (classK, typeK, constK);
name space of classes and types maintained in tsig;
read_tyname/read_const now raise ERROR instead of TYPE;
tuned;

simplified is_stale, check_stale;
fixed map_sg -- proper treatment of non-drafts;

Major cleanup:
got rid of types bclass, xclass, xsort, xtyp, xterm;
reorganized code to separate stamps/data/sign;
clarified name space inter/extern operations;
sane read/certify operations -- more picky about stale signatures;
sane implementation of signature extensions;

added the_const_type;

replaced set_naming by restore_naming;

renamed cond_extern to extern;
name entry path superceded by general naming context;
added qualified_names, no_base_names, custom_accesses, set_policy, set_naming;
replaced NameSpace.extend by context-dependent declare_name;
removed full_name';
tuned;

better error reporting

improved read_tyname;
merge_stamps, merge_refs: error instead of raise TERM;

superceded by Pure.thy and CPure.thy;

- 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.

added del_modesyntax(_i);
added print_all_data;

*** MESSAGE REFERS TO PREVIOUS VERSION ***
added declared_tyname/const and read_tyname/const;
removed certify_tyname/const;
added prep_ext_merge, nontriv_merge kept internal;
efficient subsig test;

*** empty log message ***

Further work on interpretation commands. New command `interpret' for
interpretation in proof contexts.

Removed practically all references to Library.foldr.

Move towards standard functions.

Deleted Library.option type.

tuned certify_typ/term;

tuned certify_term;

Merged in license change from Isabelle2004

avoid premature evaluation of syn_of (wastes time in conjunction with pp);

added is_logtype (replaces logtypes field of syntax); tuned merge;

proper treatment of logical types within syntax;

improved output; refer to Pretty.pp;

xxx_typ_raw replace xxx_typ_no_norm forms; prevent duplicate consts declarations in merge; misc cleanup;

reimplementation of HOL records; only one type is created for
each record extension, instead of one type for each field. See NEWS.

warning: non-identifier declaration;

support for advanced translation functions;

Printing functions now use cond_extrn instead of extrn
(due to short_names flag)

GPLed;

hide: flag for full/base name;

Syntax.read_typ: pass intern sort fn;

data: removed obsolete finish method;

clarified order of merge_lists';

merge_stamps: merge_lists' with reversed args;

theory data: finish method;

added pretty_term', read_typ', read_typ_no_norm', read_def_terms'
which refer to local syntax;

added certify_tyname;

support for absolute namespace entry paths;

added exists_stamp;
added PureN, CPureN;

added certify_tycon, certify_tyabbr, certify_const;

added typ_instance;

typ_no_norm;

fixed Thm.eq_thm: use Sign.joinable;

eta-expanded to handle value polymorphism

removed is_type_abbr;
added certify_class, certify_sort, read_sort;
adapted to inner syntax of sorts;

added simple_read_term;

made SML/NJ happy;

name space hide operations;

added is_type_abbr;

read_def_terms (no certify yet);

nodup_vars: fixed omission of 2 minor cases; account for Frees as well;

added witness_sorts, univ_witness;
removed nonempty_sort;

Type.norm_term;

err_method: pass exn;
nontriv_merge: no handle_error;

added cond_extern_table;

theory data: copy;

token translation: real;

renamed sig to PRIVATE_SIGN;

comments

PRIVATE sig parts;

Unified treatment of type error msgs.

Added a few breaks in error text.

moved long_names / cond_extern to name_space.ML;

improved data: secure version using Object.T and Object.kind;

certify_term: type_check replaces Term.type_of, providing sensible
error messages;
eliminated mapfilt_atoms (use Term.foldl_aterms);

added is_stale;

tuned comment;

tuned msg;

added defaultS: sg -> sort;
added full_name_path: sg -> string -> bstring -> string;
added add_nonterminals: bstring list -> sg -> sg;

Sign.merge vs. Sign.nontriv_merge;

fixed add_trrules: intern root;

added of_sort;

renamed Symtab.null to Symtab.empty;
renamed Symtan.extend_new to Symtab.extend;
renamed Symtan.DUPLICATE to Symtab.DUP;

tuned trfuns types;

improved error msg;

removed data.ML (made part of sign.ML);

exported pretty_classrel, pretty_arity;
added infer_types_simult;
tuned infer_types interface;
moved print_sg to display.ML;

merge_refs: check for different versions of theories;

export read_raw_typ;

adapted add_trfunsT;

type object = exn (enhance readability);

*** empty log message ***

added str_of_sg: sg -> string;
improved error handling of data access;

add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
add_term_consts, map_typ, map_term: moved from sign.ML to term.ML;

made SML/NJ happy;

self_ref: check_stale;
moved pure stuff to pure_thy.ML;

hide id, stamps;
added stamp_names_of, name_of;
replaced make_draft by prep_ext;
improved print_sg;
tuned;

certify: check_stale;

sg_ref: automatic adjustment of thms of draft theories;

tuned types;

fixed types of add_XXX;
added base_name;
tuned exports;
tuned output of sg;

fixed prep_ext;

improved pretty_arity;

make_draft replaced by prep_ext;
improved print_data;
merge now does trivial (absorptive) merges only;
added nontriv_merge;

added additional generic data;

fixed extern;
added str_of_classrel, str_of_arity, str_of_arity;

merge: drops path elements;

tuned exports;
tuned add_space;
tuned print_sg;
fixed "op ==>" syntax;

improved types of add_XXX funs (xtyp etc.);
tuned comments;
tuned msgs;
improved merge: no longer raises ERROR, but TERM;

now supports qualified names (intern vs. extern) !!!
added long_names: bool ref (initially false);
new internal forms: add_classes_i, add_classrel_i, add_defsort_i,
add_arities_i;
rep_sg: added path, spaces;
added pretty_sort (uses proper syntax);
improved print_sg;
eliminated raise_term, raise_typ;

tuned error / warning;

improved type check error messages;

renamed subclass to classrel;
tune type checking error msgs;

added add_tokentrfuns;

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

adapted to new Syntax.read_typ;

added typed print translations;

add_modesyntax(_i): added 'inout' argument;

renamed "symbolfont" to "symbols";

Eta-expansion of a function definition, for value polymorphism

restored changed prettyprinting of ==>;

added add_modesyntax(_i);
improved syntax of ==, =?=, ==> (now allows "op ...");
added Pure symbolfont syntax;

removed 'open Syntax Type';

subsig tuning;

tuned subsig;

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

Replaced foldl nodup_TVars by nodup_TVars_list -- for a big speedup on Poly/ML

Changed some mem calls to mem_string for greater efficiency (not that it could matter)

changed prettyprinting of ==>

Inserted spaces in error messages to improve readability

Translation infixes <->, etc., no longer available at top-level

Added some functions which allow redirection of Isabelle's output

Added some optimized versions of functions dealing with sets
(i.e. mem, ins, eq_set etc.) which do not use the polymorphic =
operator

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

added nodup_Vars check in cterm_of. Prevents same var with distinct types.

inserted tabs again

removed tabs

"prep_const" now calls compress_type to ensure sharing among
types of constants in theories.

exports exn_type_msg for error messages. Calls new infer_types.
Improved comments.

added same_sg and same_thm

nonempty_sort: no longer var names as args;

added (my own version of) nonempty_sort: sg -> (string * sort) list -> sort
-> bool;

Added nonempty_sort.

moved mixfix syntax to Syntax/mixfix.ML

added cargs for curried function application

added add_trrules_i;

changed pretty printing of applC

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

removed print_msg parameter of infer_types

Removed an old bug which made some simultaneous instantiations fail if they
were given in the "wrong" order.

Rewrote sign/infer_types.

Fixed some comments.

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.

fixed a bug in infer_types/exn_type_msg

added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)

added check "length ts > 1" before printing ambiguity warning in infer_types

moved ambiguity_level to Syntax/syntax.ML

added reference variable ambiguity_level to control ambiguity warnings

added optional precedence for body of binder;
removed call to infer_types from read_xrules

replaced type_syn by pure_syn in Pure signature

Pure/sign/infer_types/exn_type_msg: new, for more uniform handling of
exception TYPE

added print_msg;
added call of Type.infer_types to resolve ambiguities

exported pretty_sort;
various minor internal changes;

minor internal changes;

removed constant _constrain from Pure sig;

added pretty_sg;
added infer_types;
removed subclasses arg of add_classes;
removed old 'extend' and related stuff;
various minor internal changes;

added add_classrel;

workaround bug in Type.expand_typ;

replaced infix also by |>

added subsort, norm_sort, classes;
minor internal cleanups;

added const_type: sg -> typ option;
stamps now stored in REVERSE order;
now supports 'draft signatures' and incremental extension: is_draft,
add_classes (supports axclasses), add_defsort, add_types, add_tyabbrs,
add_tyabbrs_i, add_arities, add_consts, add_consts_i, add_syntax,
add_syntax_i, add_trfuns, add_trrules, add_name, make_draft;
added const_of_class, class_of_const (for axclasses);
changed the pure signature to support axclasses (added itself, TYPE);
various major internal changes;

fixed misfeature in Sign.extend: types of consts were read wrt. the new syntax;

*** empty log message ***

improved eq_sg;
cosmetical change in print_sg;

major cleanup;
added eq_sig;
added print_sg (full contents), pprint_sg (stamps only);
added certify_typ, certify_term;
changed read_typ: result now certified;

Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
functions from sign.ML to thm.ML or drule.ML. This allows the "prop" field
of a theorem to be regarded as a cterm -- avoids expensive calls to
cterm_of.

moved misplaced comment

added fake_cterm_of to speed up rewriting

added subsig: sg * sg -> bool to test if one signature is contained in another.

Necessary changes to accomodate type abbreviations.

Updated read_insts to approximate simultaneous type checking of substitution
pairs.

*** empty log message ***

extend: cleaned up, adapted for new Syntax.extend;
extend, merge: improved roots (logical_types) handling;

changed some names and deleted *NORMALIZED*

Sign.extend: Syntax.extend now called with read_ty;

Pure/ROOT.ML
cleaned comments;
removed extraneous 'print_depth 1';
replaced Basic_Syntax by BasicSyntax
added 'use "install_pp.ML"';

Pure/README
fixed comments;

Pure/POLY.ML
Pure/NJ.ML
make_pp: added fbrk;

Pure/install_pp.ML
replaced "Ast" by "Syntax";

Pure/sign.ML
added 'quote' to some error msgs;

Initial revision