tuned structure

add lemma

bookkeeping and input syntax for exact specification of names of symbols in generated code

use generic data for code symbols for unified "code_printing" syntax for custom serialisations

dedicated module for code symbol data

symbol data covers class relations also

merged

proper internal error, not user error;

tuned;

tuned signature;

tuned;

unify types of bound variables in the same manner as Unify.new_dpair (which emphatically "Tries to unify types of the bound variables!");

tuned signature -- slightly more general operations (cf. term.ML);

re-use Pattern.unify_types, including its trace_unify_fail option;

tuned signature; tuned comments;

improved handling of free variables' types in Isar proofs

pass noninteractive flag -- necessary to run under CASC's "runsolver" program

untabify

more lemmas for sorted_list_of_set

prefer object equality

slightly clearer formulation

interpretation must always operate on the last element in a local theory stack, not on all elements: interpretated facts must disappear after pop from local theory stack, and transfer from last target is not enough

mark local theory as brittle also after interpretation inside locales; more correct bookkeeping on brittleness: must store directly beside lthy data, with implicit default true for levels > 1; check brittleness only during context switch using (in ...) syntax, not for arbitrary exit of local theory

merged

added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;

tuned signature;

more informative Build.build_results; tuned;

stop protocol handlers as well;