weaker precendence of syntax for big intersection and union on sets

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;

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;

tuned;

less intrusive rendering of antiquoted text -- avoid visual clash with "blue variables" in particular;

proper context;

make SML/NJ happy;

added CASC-related files, to keep a public record of the Isabelle submission at the competition

disabled choice in Satallax

use HOL-TPTP image in TPTP tools (for less verbose and faster startup) and filter out some messages

prefer compiled version of LEO-II and Satallax if available

updated remote provers