clarified signature;

clarified axiom_table: uniform space (e.g. like consts), e.g. relevant for export of HOL-ex.Join_Theory;

proper theory naming after join (reset due to merge_data);

support join of anonymous theory nodes, e.g. relevant for parallel theory construction;

clarified signature;

clarified signature;

clarified document antiquotation @{theory};

clarified signature;

tuned;

clarified exception;

clarified implicit Pure.thy;

proper base name, e.g. relevant for Code_Namespace.hierarchical_program;

unused since 15865e0c5598;

PIDE reports of implicit variable scope;

more rigid check of lhs;

within a proof body context, undeclared frees are like global constants;
tuned signature;

suppress irrelevant position reports;

tuned signature: eliminated pointless type Context.pretty;

more explicit Defs.context: use proper name spaces as far as possible;

tuned signature;

eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
Object_Logic.add_judgment more like Theory.specify_const;

renamed Defs.node to Defs.item;
clarified type Defs.item;
clarified item_ord for printing;

tuned signature;

tuned whitespace;

HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
defs.ML: track dependencies also for type constructors;
typedef.ML: add type defined by typedef to dependencies, Abs and Rep now depend on the type;
Pure types and typedecls are final -- no dependencies;

more abstract theory certificate, which is not necessarily the full theory;

prefer theory_id operations;
tuned signature;

formal Theory.check, with markup and completion;

tuned signature;

eliminated pointless check -- command definitions are subject to theory context;

tuned signature;

insist in explicit overloading;

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

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;

added Theory.setup convenience;

type theory is purely value-oriented;

immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance;

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

entity markup for theory Pure, to enable hyperlinks etc.;

theory def/ref position reports, which enable hyperlinks etc.;
more official header command parsing;

more standard bootstrapping of Pure.thy;

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;

eliminated odd 'finalconsts' / Theory.add_finals;

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

explicit join_syntax ensures command transaction integrity of 'theory';

added Theory.nodes_of convenience;

recovered Theory.check_def: full name needs to be determined from background thy, not auxiliary ctxt (broken in 774df7c59508, caused Nitpick.all_axioms_of to produce bad results);

pass plain Proof.context for pretty printing;

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;

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

modernized structure Proof_Context;

tuned;

turned show_sorts/show_types into proper configuration options;

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

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

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

disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;

moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
discontinued old-style Theory.add_defs(_i) in favour of more basic Theory.add_def;
modernized PureThy.add_defs etc. -- refer to high-level Thm.add_def;

replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;

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

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

primitive defs: clarified def (axiom name) vs. description;

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

begin_theory: set theory_name here;

make SML/NJ happy;

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;

indicate CRITICAL nature of various setmp combinators;

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

renamed NameSpace.bind to NameSpace.define;

Theory.add_axioms/add_defs: replaced old bstring by binding;

Merge.

Binding.str_of;

removed Ids;

binding is alias for Binding.T

requires: check ancestors directly;

removed Table.extend, NameSpace.extend_table

cleaned up binding module and related code

simplified oracle interface;

simplified specify_const: canonical args, global deps;

type Properties.T;

moved global pretty/string_of functions from Sign to Syntax;

removed obsolete SIGN_THEORY -- no name aliases in structure Theory;
removed obsolete BASIC_THEORY;

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

apply_wrappers: perhaps_apply/loop;

Theory.specify_const: added deps argument;

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

added specify_const;

Sign.the_const_constraint;

Syntax.parse/check/read;
no export of read/cert_axm;

tuned signature;
moved generic interpretation to interpretation.ML;
added abstract at_begin/end wrappers;

introduced generic concepts for theory interpretators

new access interface in defs.ML

replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;

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

removed comments -- no exception TERM;
merge_list: exception THEORY;

tuned Pure/General/name_space.ML

simplified DataFun interfaces;

removed obsolete inferT_axm;

simplified read_axm;

tuned signature;
added axiom_table, oracle_table;
removed unused read_def_axm;

removed unused dep_graph;

removed obsolete sign_of/sign_of_thm;

added theory dependency graph

advanced translation functions: Proof.context;

added merge_list;

removed type aliases for theory/theory_ref;

dropped definitions_of

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;

tuned;

added add_deps, which actually records dependencies of consts (unlike add_finals);
tuned;

Defs.specifications_of: lhs/rhs now use typargs;

tuned Defs interfaces;

Theory.add_defs(_i): added unchecked flag;

tuned Defs.merge;

Defs.define: const_typargs;

added definitions_of;

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

tuned;

added more detailed data to consts

adapted Sign.infer_types(_simult), Sign.certify_term/prop;

moved no_vars to sign.ML;
removed dest_def (cf. Sign.cert_def);

advanced translations: Context.generic;

add_finals: prep_consts, i.e. varify type;

sane ERROR handling;

defs: beta/eta contract lhs;

tuned;

back to simple 'defs' (cf. revision 1.79);
prep_const: Compress.type;

slight adaptions to library changes

exported dest_def

Compress.term;

check_overloading replaces datatype overloading;
tuned;

tuned defs interface;

tuned;

1) all theorems in Orderings can now be given as a parameter
2) new function Theory.defs_of
3) new functions Defs.overloading_info and Defs.is_overloaded

Syntax.read thy;

renamed init to init_data;

added begin_theory, end_theory;

type theory, theory_ref, exception THEORY and related operations imported from Context;
actual theory content declared as theory data;
removed syn_of;
import theory operations in SIGN_THEORY from Sign;
tuned;

renamed hide_classes/types/consts to hide_XXX_i;
added separate hide_classes/types/consts;
refer to name spaces values instead of names;

axioms and oracles: NameSpace.table;
added axioms_of, all_axioms_of;

A flag DEFS_CHAIN_HISTORY can be used to improve the error message
in case a cycle has been detected. If it is switched off and a cycle has been
detected, the user is notified that there is such a flag.

renamed const_deps to defs;
improved error messages;
major cleanup -- removed quite a bit of dead code;

Integrates cycle detection in definitions with finalconsts

Sign.restore_naming;
err_in_defn: do not apply Sign.full_name again;
tuned;

Removed final_consts from theory data. Now const_deps deals with final
constants.

added qualified_names, no_base_names, custom_accesses, set_policy, restore_naming;
tuned;

Infinite chains in definitions are now detected, too.

Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).

added del_modesyntax(_i);

*** MESSAGE REFERS TO PREVIOUS VERSION ***
Sign.prep_ext_merge;

*** empty log message ***

Move towards standard functions.

Deleted Library.option type.

Merged in license change from Isabelle2004

Sign.is_logtype;

improved output; refer to Pretty.pp;

Type.strip_sorts;

support for advanced translation functions;

Added support for making constants final, that is, ensuring that no
definition can be given later (useful for constants whose behaviour is
fixed axiomatically rather than definitionally).

Fixed soundness bug.

Changed no_vars such that it outputs list of illegal schematic variables.

Ported find_intro/elim to Isar.

GPLed;

hide: flag for full/base name;

theory data: removed obsolete finish method;

theory data: finish method;

support for absolute namespace entry paths;

Sign.exists_stamp;

improved messages;

Sign.typ_instance;

tuned error handling;

axioms: Term.no_dummy_patterns;

tuned cycle_msg;

const_deps: unit Graph.T;
proper merge of const_deps;
tuned;

Defs are now checked for circularity (if not overloaded).

Tightened up check of types in constant defs.

adapted to inner syntax of sorts;

name space hide operations;

removed merge_theories;

prep_ext exported (again);

hide prep_ext, merge_theories;

theory data: copy;

added assert_super;

token translation: real;

added is_draft;
renamed sig to PRIVATE_THEORY;

Theory.apply replaced by Library.apply;

val copy: theory -> theory;

removed local_theory;

PRIVATE sig parts;

added read_def_axm;

tuned comments;

use Object.T and Object.kind;
added print_data;
improved get_data, put_data: more abstract;
add_axioms(_i), add_oracle: made atomic transactions;

fixed error msgs;

Changed require to requires for MLWorks

fixed comment;

renamed setup to apply;
added add_nonterminals: bstring list -> theory -> theory;
added parent_path: theory -> theory;
added root_path: theory -> theory;
added require: theory -> string -> string -> unit (from section_utils.ML);

added local_theory (for Isar);
added setup;

Sign.merge vs. Sign.nontriv_merge;

tuned add_trrules;

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

tuned trfuns types;

init_data: improved print method;

tuned infer_types interface;

adapted add_trfunsT;
defs: admit TYPE arguments;

type object = exn (enhance readability);

tuned init_data;

added ancestors;

tuned names;
tuned prep_ext_merge;

tuned;

sg_ref: automatic adjustment of thms of draft theories;

tuned types;

fixed types of add_XXX;

added merge_theories (new name arg);

remove merge_theories;
merge_list: always prepares extend -- no longer supports aliasing merges;

added init_data, get_data, put_data;

improved oracles: named, many per theory;
name spaces: thmK, oracleK;

improved types of add_XXX funs (xtyp etc.);

new internal forms: add_classes_i, add_classrel_i, add_defsort_i, add_arities_i
added add_path, add_space;
eliminated raise_term;

moved theory stuff (add_defs etc.) here from drule.ML;
only BasicTheory opened;

improved type check error messages;

added add_tokentrfuns;

added typed print translations;

add_modesyntax(_i): added 'inout' argument;

added add_modesyntax(_i);

Improved error handling: if there are syntax or type-checking
errors, prints the name of the offending axiom

Addition of oracles

New file of just the theory primitives