2013-05-22 haftmann 2013-05-22 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
2013-05-22 haftmann 2013-05-22 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
2013-05-22 wenzelm 2013-05-22 merged
2013-05-22 wenzelm 2013-05-22 added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
2013-05-22 wenzelm 2013-05-22 tuned signature;
2013-05-22 wenzelm 2013-05-22 more informative Build.build_results; tuned;
2013-05-22 wenzelm 2013-05-22 stop protocol handlers as well;
2013-05-22 wenzelm 2013-05-22 more robust command line -- accomodate /bin/kill on recent Linux (e.g. Xubuntu 13.04):
2013-05-22 wenzelm 2013-05-22 explicit management of Session.Protocol_Handlers, with protocol state and functions; more self-contained ML/Scala module Invoke_Scala;
2013-05-22 smolkas 2013-05-22 prevent pretty printer from automatically annotating numerals
2013-05-22 smolkas 2013-05-22 tuned
2013-05-22 nipkow 2013-05-22 simplified example and proof
2013-05-22 nipkow 2013-05-22 tuned
2013-05-21 wenzelm 2013-05-21 tuned messages;
2013-05-21 wenzelm 2013-05-21 proper options; tuned;
2013-05-21 wenzelm 2013-05-21 proper options;
2013-05-21 wenzelm 2013-05-21 more markup;
2013-05-21 wenzelm 2013-05-21 tuned;
2013-05-21 wenzelm 2013-05-21 less intrusive rendering of antiquoted text -- avoid visual clash with "blue variables" in particular;
2013-05-21 wenzelm 2013-05-21 proper context;
2013-05-21 wenzelm 2013-05-21 make SML/NJ happy;
2013-05-21 blanchet 2013-05-21 added CASC-related files, to keep a public record of the Isabelle submission at the competition
2013-05-21 blanchet 2013-05-21 disabled choice in Satallax
2013-05-21 blanchet 2013-05-21 use HOL-TPTP image in TPTP tools (for less verbose and faster startup) and filter out some messages
2013-05-21 blanchet 2013-05-21 prefer compiled version of LEO-II and Satallax if available
2013-05-21 blanchet 2013-05-21 updated remote provers
2013-05-21 blanchet 2013-05-21 added compatibility alias
2013-05-20 wenzelm 2013-05-20 merged
2013-05-20 wenzelm 2013-05-20 more rigorous check of simplifier context; tuned;
2013-05-20 wenzelm 2013-05-20 proper context;
2013-05-20 wenzelm 2013-05-20 proper context;
2013-05-20 wenzelm 2013-05-20 proper run-time context;
2013-05-20 wenzelm 2013-05-20 more precise treatment of theory vs. Proof.context;
2013-05-20 wenzelm 2013-05-20 proper run-time context;
2013-05-20 wenzelm 2013-05-20 tuned;
2013-05-20 wenzelm 2013-05-20 more explicit Session.update_options as source of Global_Options event;
2013-05-20 wenzelm 2013-05-20 even later Options.reset_default -- still needed for printing errors of Session.finish (e.g. via Command_Line.tool0);
2013-05-20 wenzelm 2013-05-20 tuned;
2013-05-20 wenzelm 2013-05-20 discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
2013-05-20 wenzelm 2013-05-20 reset options last -- other parts of the system may still need them;
2013-05-20 wenzelm 2013-05-20 tuned signature;
2013-05-20 blanchet 2013-05-20 updated Sledgehammer docs
2013-05-20 blanchet 2013-05-20 parse agsyHOL proofs (as unsat cores)
2013-05-20 blanchet 2013-05-20 freeze types in Sledgehammer goal, not just terms
2013-05-20 blanchet 2013-05-20 generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue)
2013-05-20 blanchet 2013-05-20 tuned code
2013-05-20 blanchet 2013-05-20 started adding agsyHOL as an experimental prover
2013-05-20 nipkow 2013-05-20 defined lvars and rvars of commands separately.
2013-05-19 blanchet 2013-05-19 made "completish" mode a bit more complete
2013-05-19 haftmann 2013-05-19 infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
2013-05-19 haftmann 2013-05-19 tuned and clarified
2013-05-19 haftmann 2013-05-19 tuned, including signature
2013-05-18 wenzelm 2013-05-18 discontinued odd workaround for scala-2.10.0-RC1;
2013-05-18 wenzelm 2013-05-18 discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
2013-05-18 wenzelm 2013-05-18 explicit notion of public options, which are shown in the editor options dialog; avoid hard-wired stuff;
2013-05-17 wenzelm 2013-05-17 back to more paranoid interrupt test after request is cancelled -- avoid race condition;
2013-05-17 wenzelm 2013-05-17 timeout counts as regular error, with rc = 1 (cf. special Exn.Interrupt vs. regular TimeLimit.TimeOut in Isabelle/ML);
2013-05-17 wenzelm 2013-05-17 added isabelle tty option -o;
2013-05-17 wenzelm 2013-05-17 oops;
2013-05-17 wenzelm 2013-05-17 renamed 'print_configs' to 'print_options';