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;

more robust command line -- accomodate /bin/kill on recent Linux (e.g. Xubuntu 13.04):

explicit management of Session.Protocol_Handlers, with protocol state and functions; more self-contained ML/Scala module Invoke_Scala;

prevent pretty printer from automatically annotating numerals

tuned

simplified example and proof

tuned

tuned messages;

proper options; tuned;

proper options;

more markup;