some uses of "' " as witness for this feature;

clarified signature;

avoid global syntax for MinProof (amending e31271559de8);

global declaration of abstract syntax for proof terms, with qualified names;
clarified modules;

eliminated ASCII syntax from Pure bootstrap;
tuned comments;

notation for dummy sort;

more symbols;

prefer hardwired "nothing";

explicit property for unbreakable block;

clarified simple mixfix;

more position information for type mixfix;

clarified treatment of fragments of Isabelle symbols during bootstrap;

discontinued \<struct> syntax;

former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
uniform syntax for Pure.imp;
removed obsolete "HTML" syntax;

tuned signature;

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

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;

eliminated \<Colon> from syntax of constraints;

discontinued old "xnum" token category;
simplified Lexicon.read_num, Lexicon.read_float: no sign here;
express ZF numerals via "num" with mixfix grammar;
recovered printing of ZF numerals: "one" is abbreviation;

more source positions;

more qualified names;

more qualified names;

more qualified names;

more qualified names;

tuned signature;

tuned signature;

produce qualified names more directly;

inner syntax token language allows regular quoted strings;
tuned signature;

support for nested text cartouches;
clarified Symbol.is_symbolic: exclude \<open> and \<close>;

added Theory.setup convenience;

explicit support for type annotations within printed syntax trees;
eliminated obsolete show_free_types;

tuned;

tuned signature;

syntax translations always depend on context;

added var_position in analogy to longid_position, for typing reports on input;
avoid duplicate token var report;

uniform notation for == and \<equiv> (cf. 3e3c2af5e8a5);

removed odd associativity of ==

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;

renamed "xstr" to "str_token";

position constraints for numerals enable PIDE markup;

renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";

inner syntax positions for string literals;

discontinued numbered structure indexes (legacy feature);

special treatment of structure index 1 in Pure, including legacy warning;

less bulky "_position", for improved readability of parse trees;

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

discontinued Syntax.max_pri, which is not really a symbolic parameter;

CONST syntax with positions;

moved CONST syntax/translations to their proper place;

simplified Pure syntax bootstrap;

renamed sprop "prop#" to "prop'" -- proper identifier;
eliminated spurious symbolic string bindings (logic, any etc.);
hardwired special "prop" vs. "prop'" conversion;
tuned;

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

explicit structure Syntax_Trans;
discontinued old-style constrainAbsC;

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

type syntax as regular mixfix specification (type_ext for bootstrapping has been obsolete for many years);

moved unparse material to syntax_phases.ML;

more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;

support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
simplified/generalized abs_tr/binder_tr: allow iterated constraints, stemming from positions;
Ast.pretty_ast: special treatment of encoded positions;
eliminated Ast.str_of_ast in favour of uniform Ast.pretty_ast;

renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;

--HG--
rename : src/Pure/pure_thy.ML => src/Pure/global_theory.ML

tuned signature of (Context_)Position.report variants;

actually declare "_constrainAbs" as @{syntax_const};

modernized some structure names, keeping a few legacy aliases;

renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;

Thm.add_axiom/add_def: return internal name of foundational axiom;

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 PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;

minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';

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;

slightly more abstract syntax mark/unmark operations;

authentic syntax for *all* term constants;

moved generic update_name to Pure syntax -- not specific to HOL/record;

renamed InfixName to Infix etc.;

eliminated obsolete thm position tags;

adapted Theory_Data;
tuned;

modernized structure Simple_Syntax;

set Pure theory name properly

maintain group via name space, not tags;

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

eliminated dead code;

join_proofs: implicit exception;
removed obsolete cancel_proofs, cf. cancel_thy in thy_info.ML;
tuned;

cancel_proofs: some attempts at reworking group management (based on body promises only);

tuned signature;

more uniform handling of binding in targets and derived elements;

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

Merge.

Thm.binding;

use long names for old-style fold combinators;

binding replaces bstring

added cancel_proofs, based on task groups of "entered" proofs;

tuned;

simplified join_proofs;

renamed terminal category "float" to "float_token", to avoid name
space conflicts with actual "float" types in user theories (only
"float_const" is encountered in practice anyway);
tuned;

renamed force_proofs to join_proofs;

renamed type Lazy.T to lazy;
force_proofs: original order;

cleaned up binding module and related code

new Binding module

New lexical item "float".

fact table now using name bindings

using name bindings

Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;

added force_proofs (based on thms ever passed through enter_thms);

renamed Thm.get_axiom_i to Thm.axiom;

added const sort_constraint with syntax SORT_CONSTRAINT -- logically vacous;

name_thm etc.: pass position;
note_thms etc.: Name.binding, report fact_decl;

moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);

get_fact: report position;

removed obsolete note_thms_cmd;

PureThy: dropped note_thmss_qualified, dropped _i suffix

dropped PureThy.note; added PureThy.add_thm

removed old theorem database;

theory Pure provides regular application syntax by default;
added old_appl_syntax_setup for former Pure clients;

renamed check_fact to defined_fact;

removed obsolete get_fact_silent;
PureThy.get_fact: pass dynamic context;
tuned;

added intern_fact, check_fact, hide_fact;
renamed all_facts_of to facts_of;
removed hide_thms;
Sign.hide_const;

moved forall_elim_var(s) to more_thm.ML;
get_thm(s) and hide_thms: use new table;

rep_cterm/rep_thm: no longer dereference theory_ref;

removed obsolete add_axiomss(_i);

eliminated destructive/critical theorem database;
simplified store_thm(s);
removed obsolete smart_store_thm(s);
tuned;

NAMED_CRITICAL;

Context.>> : operate on Context.generic;

tuned;

removed obsolete appl_syntax, applC_syntax;

eliminated theory ProtoPure;
implicit setup of emerging theory Pure;

get fact: do not compare names;

support dynamic facts;

get_thms etc.: improved reporting of source position;

Facts.Named: include position;

simplified get_thm(s): back to plain name argument;
renamed former get_thms(_silent) to get_fact(_silent);

renamed datatype thmref to Facts.ref, tuned interfaces;

removed check_lookup;
added get_thms_silent;

added ckeck_lookup flag (default false), which controls sanity check of thm lookup;

Facts.add_global;

get_thm(s): check facts lookup vs. old thm database;

replaced obsolete FactIndex.T by Facts.T (cumulative version, assumes that facts are only added to unfinished theories);
removed unused get_thm(s)_closure;
removed obsolete fact_index_of, valid_thms, thms_containing(_consts);

maintain default position;

added theorem group operations;
note_thmss: add kind to *all* intermediate thms;
get_kind: default to empty name;

added simple primitive note

replaced obsolete Theory.add_finals_i by Theory.add_deps;

removed obsolete simple_def;

removed unused add_defss;

NameSelection: more interval checks;

Sign.add_consts_authentic: tags (Markup.property list);

tuned functor application;

added simple definition scheme

moved appl syntax to PureThy;
SimpleSyntax.read_typ/term/prop;

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

removed dead code;

marked some CRITICAL sections;

thm tag: Markup.property list;

simplified DataFun interfaces;

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

Thm.internalK;

removed obsolete theorem_space;

added has_kind/get_kind;
tuned;

proper use of PureThy.has_name_hint instead of hard-wired string'';

Expose hard-wired string which was changed and broke Proof General.

moved thm/thms to ml_context.ML;
moved generic_setup, add_oracle to isar_cmd.ML;

adapted ML context operations;

added has_name_hint;
name_thm: more careful pre-naming;

thm/prf: separate official name vs. additional tags;

Theory.merge_list;

*** bad commit -- reverted to previous version ***

added map/burrow_facts;
exported name_multi, name_thm;

added map/burrow_facts;
exported name_multi, name_thm;

added burrow_fact;
no export of name_thms(s);

updated (binder) syntax/notation;

tuned;

moved theorem kinds from PureThy to Thm;
exported note_thms(s);

*** empty log message ***

member (op =);

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

tuned exception handling;

support embedded terms;

added add_defs_unchecked(_i);

added syntax for _type_constraint_;

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

tuned;

moved print_theorems/theory to Isar/proof_display.ML;

Term.itselfT;

avoid polymorphic equality;

simplified Pure conjunction, based on actual const;

removed distinct, renamed gen_distinct to distinct;

proper order of trfuns;

moved theorem tags from Drule to PureThy;
replaced kind attribute by kind string;
tuned name_multi: index > 1 only;
added note_thmss_qualified (from Isar/locale.ML);

export name_multi;

simplified type attribute;

setup: theory -> theory;
added syntax (from Syntax/mixfix.ML);
added HTML output syntax for _lambda;

sane ERROR handling;

generic_setup: optional argument, defaults to Context.setup();

gen_names: preserve empty names;

re-arranged tuples (theory * 'a) to ('a * theory) in Pure

oriented result pairs in PureThy

re-oriented some result tuples in PureThy

datatype thmref: added Fact;
renamed Goal constant to prop;

added thm(s) retrieval functions (from goals.ML);

Theory.add_finals_i;

slight adaptions to library changes

TableFun/Symtab: curried lookup and update;
add_defs etc.: use Thm.get_axiom_i, which is independent from naming;

added generic_setup, add_oracle (from isar_thy.ML);

curried_lookup/update;

export theorems_of;

Compress.init_data;

(intermediate commit)

tuned forall_elim_var(s): avoid expensive Term.add_vars;

renamed init to init_data;

enter_thms: use theorem database of thy *after* attribute application;

datatype thmref = Name ... | NameSelection ...;
added print_theorems_diff;
tuned;

added theorem_space;
removed unused extern_thm_sg;
accomodate change of TheoryDataFun;
accomodate identification of type Sign.sg and theory;
removed theory management (cf. 'history' in context.ML);
moved add_typedecls to sign.ML;
Sign.init, Theory.init;
tuned;

thms_of no longer global;
added all_thms_of;
theorems: NameSpace.table;

renamed cond_extern to extern;
removed note_thmss_accesses(_i) -- functionality covered by general naming context;

added string_of_thmref, selections, fact_index_of, valid_thms;
moved find_matching_thms, is_matching_thm, find_intros/intros_goal/elims to Isar/find_theorems.ML;
tuned

moved credit to CONTRIBUTORS;

searching for thms by combination of criteria (intro, elim, dest, name, term pattern)

credits

new thms_containing that searches for patterns instead of constants
(by Rafal Kolanski, NICTA)

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.

*** MESSAGE REFERS TO PREVIOUS VERSION ***
added datatype interval, improved thm selections;

*** empty log message ***

First release of interpretation commands.

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

Move towards standard functions.

Deleted Library.option type.

Fixed bug in select_thm.

Subscripts for theorem lists now start at 1.

Specific theorems in a named list of theorems can now be referred to
via indices (type thmref).

fixed bug in find functions that I introduced some time ago.

Merged in license change from Isabelle2004

removed obsolete sort 'logic';

commented

renamed have_thms to note_thms;

Removed "duplicate fact binding" error message.

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

Moved find_intros_goal from goals.ML to pure_thy.ML

Fixed name clash problem in forall_elim_var.

Removed flexpair_def.

Ported find_intro/elim to Isar.

disallow duplicate fact bindings for drafts (i.e. within new-style theory files);

tuned;

improved thms_containing (use FactIndex.T etc.);

Theorems are only "pre-named" if the do not already have names.

have_thmss vs. have_thmss_i;

added hide_thms;

theory data: removed obsolete finish method;

trfuns *after* binder syntax;

Further restructuring of theorem naming functions.

renamed open_smart_store_thms to smart_store_thms_open;
added Syntax.pure_syntax_output;

theory data: finish method;

- enter_thmx -> enter_thms
- improved naming of theorems: enter_thms now takes functions pre_name and post_name
as arguments

internal thm numbering with ":" instead of "_";

Added equality axioms and initialization of proof term package.

eliminated GOAL syntax;

Syntax.pure_appl_syntax declared as output syntax for theory ProtoPure;

Display.pretty_thm_sg;

added get_thm_closure;

added get_thms_closure, single_thm;

dummy_pattern moved to term.ML;

add_defs(_i): overloaded option;

added "nothing" (empty list of theorems);

print_theorems: omit name space;

have_thmss: handle multiple lists of arguments;

get_thm(s): automatic transfer;

Pretty.chunks;

add_thms, add_axioms, add_defs: return theorems as well;

Goal: tuned pris;

dummy_pattern: aprop;

forall_elim_var(s) move here from drule.ML;
add_axioms/defs: forall_elim_vars on result;

theorem database now also indexes constants "Trueprop", "all",
"==>", "=="; thus thms_containing, findI etc. may retrieve more rules;

fixed naming of single axioms;

removed thms_closure (unused);

eliminated default_name (thms no longer stored for name "");

smart_store_thms;

tuned Goal syntax;

thms_containing: undeclared consts error;

cond_extern_table;

fixed BUG in have_thmss: return thy';

avoid string constants;

backup replaced by checkpoint;

backup operation replaces transaction;

transaction: Theory.copy;

renamed 'dummy' to 'dummy_pattern' (less dangerous);

theory data: copy;
consts dummy :: 'a ("'_");

added cond_extern_thm_sg;
have_thmss: name made optional;

workaround default_name problem;

tuned signature;

eliminated tthm type and Attribute structure;

added new print_mode "xsymbols" for extended symbol support
(e.g. genuiely long arrows)

no warning for "it" theorems;

added default_name;
added have_tthmss;

Attribute.thms_of;

Symtab.foldl;

added get_tthmss;

added store_tthm;

removed global_names flag;

moved long_names / cond_extern to name_space.ML;

tuned transaction;
moved actual (C)Pure theories to pure.ML;

Goals may now contain assumptions, which are not returned.
This is controlled by an argument `atomic' to the goal commands.

tuned transaction;

moved add_axioms_x, add_defs_x to Isar/isar_thy.ML;

use type-safe theory data interface;

added print_theorems: theory -> unit;
added print_theory: theory -> unit;
added transaction mechanism as last resort to accomodate non-atomic
transformers (please avoid such things);
tuned setup;

added get_name, put_name, global_path, local_path, begin_theory,
end_theory;

added add_axioms_x, add_defs_x;

added thms_closure: theory -> xstring -> tthm list option;
added add_typedecls: (bstring * string list * mixfix) list -> theory -> theory;
|> Theory.add_nonterminals Syntax.pure_nonterms;

tuned names of (add_)store_XXX functions;
added attributes to add_thms, add_axioms, add_defs functions;

type_error;

added Goal_def;

added get_tthm(s), store_tthms(s);
tuned;

tuned msgs;

pretty_name_space;

renamed Symtab.null to Symtab.empty;

improved theorems print method: transfer_sg;

type object = exn (enhance readability);

made SML/97 happy;

tuned thy_data;

tuned;

added ignored_consts, thms_containing, add_store_axioms(_i),
add_store_defs(_i), thms_of;
tuned pure thys;

oops;

renamed put_* to store_*;

oops, swap warnings;

Init 'theorems' data. The Pure theories.