Refute: Distinguish between "genuine" and "potential" in the newly added "expect" option.

minimal adaptions for abstract binding type;

more uniform handling of binding in packages;

more uniform handling of binding in targets and derived elements;

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

moved Thm.def_name(_optional) to more_thm.ML; moved old-style Thm.get_def to Drule.get_def;

adapted Syntax.const_name;

canonical argument order for type_name, const_name;

added const_binding;

added prefix_name, suffix_name; added eq_name; added opaque signature constraint to prevent accidental equality test;

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

renamed rep_ss to MetaSimplifier.internal_ss;

Binding.str_of: removed verbose feature, include qualifier in output; renamed Binding.add_prefix to Binding.prefix;

oracle: proper name position, tuned;

merged

drop poisonous code equations

suppress document output

theory with syntax for lattice operations

added babel -- necessary for bind infix syntax

added enumeration of predicates

moved instance option :: finite to Option.thy

constructive version of Cantor's first diagonalization argument

equalities for Min, Max

merged

added lemma

merged

Docs

eliminated Output.immediate_output -- violates the official message channel protocol;

schedule_seq: handle after_load errors as in schedule_futures;

replaced archaic use of rep_ss by Simplifier.mksimps;