prefer control symbol antiquotations;

one single plugin for code type declarations avoids problems when bootstrapping new plugins over types which have been both declared concrete and abstract in their code historiy

--HG--
extra : rebase_source : cee78bc80639b412735c3fc958b0f6e77fe5d1b3

simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
sufficient to keep history stamps rather than complete historized data;
semantically conflicting specifications are temoprary blacklisted after theory merge but remain historized;
clarified signature;

--HG--
extra : rebase_source : 8ff5c1572bfcccdd9c89eeaecbf6b7fb1af30b6d

proper concept of code declaration wrt. atomicity and Isar declarations

--HG--
extra : rebase_source : adb08da85e01b6c9c81d471a0d8e7ebb68d7e472

stripped unused / obsolete material

--HG--
extra : rebase_source : 40c0097ce275642ad1b612b828b39d3af7d2ee19

more tight filtering;

explicit tagging of code equations de-baroquifies interface

--HG--
extra : rebase_source : 1d83d31f669dc30b586df508a64fdc3a9e7b2655

clarified check_open_spec / read_open_spec;
allow 'for' fixes in 'abbreviation', 'definition';

delegate inclusion of required dictionaries to user-space instead of half-working magic

clarified naming conventions and code for code evaluation sandwiches

support 'assumes' in specifications, e.g. 'definition', 'inductive';
tuned signatures;

tuned;

droppen diagnostic junk from 4b53042d7a40

explicit computation of sort arguments for code equations makes less assumption about sort arguments of underlying type class instances

--HG--
extra : rebase_source : 02b003d36b0541e2f72489c69aeefbd5fbe4e356

tuned signature;

Thm.cterm_of and Thm.ctyp_of operate on local context;

tuned -- more explicit use of context;

eliminated some clones of Proof_Context.cterm_of

proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;

modernized and more uniform style

tuned;

proper exception for internal program failure, not user-error;

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

syntactic means to prevent accidental mixup of static and dynamic context

--HG--
extra : rebase_source : 5713560aaa0dd320d68157ba353db0f597594d25

modernized setups

degeneralized value command into HOL

--HG--
rename : src/Tools/value.ML => src/HOL/Tools/value.ML

more qualified names;

prefer proof context over background theory

--HG--
extra : rebase_source : 307a2e54d5c0b89d8668ce99110df0538037668e

spelling

more standard module name Axclass (according to file name);

more direct Sorts.has_instance;
tuned Sorts.mg_domain;

tuned signature;
tuned;

added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
tuned;

tuned signature: Name.invent and Name.invent_names;

simplified check/uncheck interfaces: result comparison is hardwired by default;
tuned;

modernized structure Proof_Context;

misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;

avoid slightly odd Conv.tap_thy

simplified evaluation function names

keep type variable arguments of datatype constructors in bookkeeping

dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term

full palette of dynamic/static value(_strict/exn)

Factored out ML into separate file