get rid of "show_all_types" in Nitpick

tuning

killed dead argument

tuning

generalized "mk_co_iter" to handle mutualized (co)iterators

tuning

tuned

tuned

merged

tuned

merged

position constraint for bound dummy -- more PIDE markup;

position constraint for dummy_pattern -- more PIDE markup;

tuned;

tuned signature;

tuned -- less ML compiler warnings;

more robust variant_free: avoid clash with consts name space (e.g. consts "x", "xa", etc.);

more uniform context;

tuned signature;

more conventional pretty printing; more markup;

tuned white-space;

more specific structure for registration into theory and dependency onto locale

examples for interpretation into target

disable SPASS's splitting if Isar proofs are desired, because these are not handled by the proof reconstruction code (and it's not clear how to handle them considering the lack of documentation)

handle lambda-lifted problems in Isar construction code

simpler proof through custom summation function

merged

tuned;

tuned;

tuned;

tuned;

syntax translations always depend on context;

updated keywords;

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

added compatibility alias

merged

more rigorous check of simplifier context; tuned;

proper context;

proper context;

proper run-time context;

more precise treatment of theory vs. Proof.context;

proper run-time context;

tuned;

more explicit Session.update_options as source of Global_Options event;

even later Options.reset_default -- still needed for printing errors of Session.finish (e.g. via Command_Line.tool0);

tuned;

discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;

reset options last -- other parts of the system may still need them;

tuned signature;

updated Sledgehammer docs

parse agsyHOL proofs (as unsat cores)

freeze types in Sledgehammer goal, not just terms

generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue)

tuned code

started adding agsyHOL as an experimental prover

defined lvars and rvars of commands separately.

made "completish" mode a bit more complete

infrastructure for generic data for code symbols (constants, type constructors, classes, instances)

tuned and clarified

tuned, including signature

discontinued odd workaround for scala-2.10.0-RC1;

discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;

explicit notion of public options, which are shown in the editor options dialog; avoid hard-wired stuff;

back to more paranoid interrupt test after request is cancelled -- avoid race condition;

timeout counts as regular error, with rc = 1 (cf. special Exn.Interrupt vs. regular TimeLimit.TimeOut in Isabelle/ML);

added isabelle tty option -o;

oops;

renamed 'print_configs' to 'print_options';

proper option quick_and_dirty;

retain quick_and_dirty as-is -- no censorship;

more system-atic options;

added isabelle-process option -o;

more precise "eval", cf. isabelle build;