backed out changeset 1b8858f4c393: odd problems e.g. in CAVA_LTL_Modelchecker;

clarified modules: more direct data implementation;

clarified modules: inference kernel maintains sort algebra within the logic;

more elementary treatment of standard_vars (unconstrainT is already standard);

tuned;

removed unused material;

trim context of persistent data;

clarified context, notably for internal use of Simplifier;

prefer regular context update, to allow continuous editing of Pure;

tuned signature: eliminated pointless type Context.pretty;

tuned signature;

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

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;

tuned signature;

tuned signature;

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

tuned signature -- prefer qualified names;

Goal.prove_multi is superseded by the fully general Goal.prove_common;

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

tuned signature to make axiomatizations more easy to spot in the source, via "add_axioms" or "axiomatization";

conceal somewhat obscure internal facts, e.g. relevant for 'print_theorems', 'find_theorems';

discontinued axiomatic 'classes', 'classrel', 'arities';

uniform orientation of instances as (type constructor, type class)

proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;

added Theory.setup convenience;

type theory is purely value-oriented;

standardized aliases;

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

formal proof context for axclass proofs;
avoid global_simpset_of -- refer to simpset of proof context;

tuned;

tuned -- prefer high-level Table.merge with its slightly more conservative update;

more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
transfer theorems where they are picked from the theory;
tuned;

tuned comment -- do not claim anything;

refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;

tuned signature: Name.invent and Name.invent_names;

pass plain Proof.context for pretty printing;

simplified pretty printing context, which is only required for certain kernel operations;
disentangled dependencies of structure Pretty;

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

modernized structure Proof_Context;

renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;

--HG--
rename : src/Pure/meta_simplifier.ML => src/Pure/raw_simplifier.ML

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

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;

tuned whitespace

avoid store flag in add_* operations

do not expose store flag of AxClass.add_*

classrel and arity theorems are now stored under proper name in theory. add_arity and
add_classrel take extra boolean argument indicating whether theorems should be stored.

eliminated redundant runtime checks;

normalize atyp names after unconstrainT, which may rename atyps arbitrarily;

the_classrel/the_arity: avoid Thm.transfer for proofterm version -- theory might already have become stale within the proof_body future;

just one version of Thm.unconstrainT, which affects all variables;
temporary workaround for Nbe.lift_triv_classes_conv;

back-patching of axclass proofs;

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

made SML/NJ happy;

removed obsolete sanity check -- Sign.certify_sort is stable;

tuned signature;

tuned classrel completion -- bypass composition with reflexive edges;

tuned diff_classrels -- avoid slightly inefficient Symreltab.keys;

tuned aritiy completion -- slightly less intermediate data structures;

clarified proven results: store thm only and retrieve proof later via Thm.proof_of (this may also impact parallelism, because internal join_proofs is deferred);

misc tuning and simplification;

removed unused AxClass.class_intros;

renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp;
less pervasive names;

more systematic treatment of data -- avoid slightly odd nested tuples here;
tuned;

replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;

misc tuning and simplification;

simplified some private bindings;

classrel and arity completion by krauss/schropp;

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

Sorts.of_sort_derivation: do not use slow Graph.irreducible_paths here, which not always needed (SUBTLE CHANGE IN SEMANTICS);
officially export weaken as Sorts.classrel_derivation;
tuned comments;

removed unused AxClass.of_sort derivation;

inlined version of old-style Drule.add_axioms -- Specification.axiom is not bootstrapped yet;

replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;

Logic.mk_of_sort convenience;

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

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

Thm.def_binding;

axclass: more precise treatment of naming vs. binding;

renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;

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

dropped some unused bindings

--HG--
rename : src/HOL/Tools/Datatype/datatype.ML => src/HOL/Tools/Datatype/datatype_data.ML
extra : rebase_source : f9974e246b201df041a994a3a755319b83bce2a3

eliminated obsolete/unused Thm.kind_internal/is_internal etc.;

conceal internal bindings;

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;

explicit close_derivation

indicate CRITICAL nature of various setmp combinators;

removed dead code;
Sorts.of_sort_derivation: removed unused pp;

modernized Balanced_Tree;

Goal.finish: explicit context for printing;

add_classrel/arity: strip_shyps of stored result;

clarified Thm.of_class/of_sort/class_triv;

renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;

renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);

tuned class user space type system code

avoid potential problem with stale theory

formal declaration of undefined parameters after class instantiation

coherent binding policy with primitive target operations

renamed sticky_prefix to mandatory_path;

replaced old-style add_path/no_base_names by sticky_prefix;

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

more uniform handling of binding in targets and derived elements;

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

explicit error message for `improper` instances lacking explicit instance parameter constants

Merge.

Thm.binding;

binding replaces bstring

close derivation of classrels

cleaned up binding module and related code

Sign.declare_const: Name.binding;

explicit type Name.binding for higher-specification elements;

completing arities after subclass instance

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

PureThy: dropped note_thmss_qualified, dropped _i suffix

dropped PureThy.note; added PureThy.add_thm

Sorts.weaken: abstract argument;

explicit completions of arities

refined arity property concept

tagged arities

moved global pretty/string_of functions from Sign to Syntax;

removed obscure "attach" feature

exported suffix

better error reporting

exported axiomsN

error handling for pathological cases

moved instance parameter management from class.ML to axclass.ML

naming policy for instances

moved define_class_params to Isar/class.ML;
removed obsolete params_of_class, print_axclasses;
moved ProofContext.pp to Syntax.pp;
misc tuning;

renamed AxClass.get_definition to AxClass.get_info (again);
AxClass.axiomatize: renamed XXX_i to XXX, and XXX to XXX_cmd;

generic Syntax.pretty/string_of operations;

replaced AxClass.param_tyvarname by Name.aT;

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

Sign.add_const_constraint;

Sign.minimize/complete_sort;

proper Sign operations instead of Theory aliases;

tuned;

clarified class interfaces and internals

avoid low-level tsig;

balanced conjunctions;
added split_defined (from conjunction.ML);

simplified DataFun interfaces;

moved axclass module closer to core system

Thm.fold_terms;

renamed of_sort_derivation record fields (avoid clash with Alice keywords);

syntax for "class attach const"

cleanup

replaced Sign.classes by Sign.all_classes (topologically sorted);

dropped some bookkeeping

tuned msg;

fixed misleading error message

code clarifications

reorganized structure Goal vs. Tactic;

completed class parameter handling in axclass.ML

Logic.name_classrel/arities;

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

Thm.adjust_maxidx;

class_of_param instead of class_of

Goal.prove: context;

added lookup function for parameters

axiomatize class: Theory.add_deps;

class axiomatization: finals;

more abstract interface to classes/arities;

removed 'concl is' patterns;

of_sort: explicit cache value;
simplified internal representation of instances;

tuned;

of_sort: option;
of_sort: simplified implementation, use Sorts.of_sort_derivation;
tuned;

of_sort: simplified derivation;

renamed add_axclass(_i) to define_axclass(_i);
renamed get_info to get_definition;
added axiomatize_class/classrel/arity (supercede Sign.add_classes/classrel/arities);
tuned;

instances data: mutable cache;
added of_sort: interface for derived instances;

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

get_info: removed 'super' field;
added params_of, all_params_of;
removed params_of_sort;
tuned;

reworded add_axclass(_i): canonical specification format,
purely definitional version,
always qualify intro/axioms;

moved abstract syntax operations to logic.ML;
maintain class parameters;
added params_of_sort;
added cert/read_classrel (from sign.ML), check class parameters;
tuned;

fixed value restriction

add_axclass(_i): return class name only;
subclass/arity statements: require actual TVars, store raw data;
tuned;

moved read_class, read/cert_classrel/arity to sign.ML;
axclass: moved outer syntax to isar_syn.ML;
instance: moved to Tools/class_package.ML;
simplified interfaces;
tuned;

Reverted to old interface of AxClass.add_inst_arity(_i)

renamed class_axms to class_intros;

moved intro_classes from AxClass to ClassPackage

renamed gen_duplicates to duplicates;

Logic.const_of_class/class_of_const;

moved instance Isar command to class_package.ML

moved theorem tags from Drule to PureThy;

exported after_qed for axclass instance

simplified type attribute;

setup: theory -> theory;

sane ERROR handling;

exported read|cert_arity interfaces

Tactic.precise_conjunction_tac;

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

oriented result pairs in PureThy

simplified after_qed;

Goal.prove;

removed obsolete axclass_tac, add_inst_subclass_x, add_inst_arity_x;

goal statements: accomodate before_qed argument;

minor tweaks for Poplog/ML;

Theory.add_finals_i;

slight adaptions to library changes

TableFun/Symtab: curried lookup and update;

tuned Isar interfaces;
tuned IsarThy.theorem_i;

name space prefix is now "c_class" instead of just "c";
export get_info;
tuned;

curried_lookup/update;

OuterKeyword;

exported after_qed for arity proofs

After_qed takes result argument.

get_thm(s): Name;

accomodate change of TheoryDataFun;
accomodate identification of type Sign.sg and theory;

refer to name spaces values instead of names;

got rid of bclass, xclass;

Theory.restore_naming;

renamed cond_extern to extern;

tuned;

sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
keep legacy stuff separate;
tuned;

export intro_classes_tac;

superceded by Pure.thy and CPure.thy;

*** MESSAGE REFERS TO PREVIOUS VERSION ***
Attrib.src;

*** empty log message ***

First release of interpretation commands.

First version of global registration command.

Move towards standard functions.

Deleted Library.option type.

Adapted to modified interface of PureThy.get_thm(s).

Merged in license change from Isabelle2004

removed obsolete sort 'logic';

improved output;

test_classrel/arity improve error reporting; tuned;

improved Term.invent_names;

'instance' and intro_classes now handle general sorts;

got rid of explicit marginal comments (now stripped earlier from input);

simplified IsarThy.theorem_i;

Term.invent_type_names;

tuned;

theory data: removed obsolete finish method;

theory data: finish method;

IsarThy.theorem_i (None, []);

IsarThy.theorem_i: no locale;

removed obsolete goal_subclass, goal_arity;

sane internal interfaces for instance;

IsarThy.theorem_i Drule.internalK;

proper use of invent_names;

tuned headers;

invent_names

support \<subseteq> syntax in classes/classrel/axclass/instance;

Tactic.distinct_subgoals_tac moved to internal intro_classes_tac;

default_intro_classes_tac: Tactic.distinct_subgoals_tac;

tuned IsarThy.theorem_i;

intro_classes by default;

Display.pretty_thm_sg;

eta-expanded to handle value polymorphism

adapted to inner syntax of sorts;

Pretty.chunks;

intrn_arity: reject type abbreviations;

HEADGOAL;

intro_classes_tac: REPEAT_ALL_NEW;

adapted to new PureThy.add_thms etc.;

expand_classes renamed to intro_classes;

propp: 'concl' patterns;

formal comments (still dummy);

outer syntax keyword classification;
no open OuterParse;

improved errors;

theory data: copy;

qualify Theory.sign_of etc.;

theory data;
attributes for class axioms;
instance_subclass/arity_proof(_i);
expand_classes proof method;
'axclass' / 'instance' outer syntax;

eliminated Attribute structure;

quiet_mode, message;

witnesses: lookup stored thms instead of axioms;

tuned msg;

adapted to new PureThy.add_axioms_i;

add_store_axioms_i;

removed add_thms_as_axms;

tuned types;

fixed goal_XXX;

fixed types of add_XXX;
tuned;

uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity;

fixed axiom names;

eliminated raise_term, raise_typ;
new internal forms: add_inst_subclass_i, add_inst_arity_i;

fully qualified names: Theory.add_XXX;

added "Proving ..." msgs;

eliminated freeze_vars;

Sorts.str_of_arity;

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

Replaced map...~~ by ListPair.map

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

adapted to new version of shyps-stuff;

modified prep_thm_axm to handle shyps;
fixed class_axms: class_trivs *first*;
improved axclass_tac: now also handles object rules as witnesses;

minor fix: instance now raises error if witness axioms don't exist;

instance: now automatically includes defs of current thy node as witnesses;

prove_subclass, prove_arity now exported;
minor internal changes;

cleaned sig;
removed add_defns (now in drule.ML as add_defs);
removed add_sigclass;
minor internal changes;

added experimental add_defns (actually should be moved somewhere else);
minor internal changes;

added functor signature constraint;

various minor changes (names and comments);

(beta release)

axiomatic type class 'package' for Pure (alpha version);