2010-10-26 krauss basic documentation for command partial_function
2010-10-26 krauss remove outdated "(otherwise)" syntax from manual
2010-10-26 krauss declare recursive equation as ".simps", in accordance with other packages
2010-10-26 haftmann merged
2010-10-26 haftmann dropped accidental doubled computation
2010-10-26 boehmes optionally force the remote version of an SMT solver to be executed
2010-10-26 boehmes tuned
2010-10-26 boehmes added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
2010-10-26 boehmes changed SMT configuration options; updated SMT certificates
2010-10-26 boehmes joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
2010-10-26 boehmes keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
2010-10-26 blanchet merged
2010-10-26 blanchet merge
2010-10-26 blanchet clearer error messages
2010-10-26 blanchet renaming
2010-10-28 wenzelm back again to non-Apple font rendering (cf. 4977324373f2);
2010-10-28 wenzelm dock isabelle-session at bottom (again, cf. 37bdc2220cf8) to ensure that controls are fully visible;
2010-10-26 wenzelm disable broken popups for now;
2010-10-26 wenzelm tuned;
2010-10-26 wenzelm do not handle arbitrary exceptions;
2010-10-26 wenzelm merged
2010-10-26 haftmann Code_Runtime.trace
2010-10-26 wenzelm proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
2010-10-26 wenzelm merged
2010-10-26 blanchet improved English
2010-10-26 blanchet whitespace tuning
2010-10-26 blanchet no need to encode theorem number twice in skolem names
2010-10-26 blanchet tuning
2010-10-26 blanchet make SML/NJ happy
2010-10-25 bulwahn relaxing the filtering condition for getting specifications from Spec_Rules
2010-10-25 bulwahn adding new predicate compiler files to the IsaMakefile
2010-10-25 bulwahn using mode_eq instead of op = for lookup in the predicate compiler
2010-10-25 bulwahn renaming split_modeT' to split_modeT
2010-10-25 bulwahn options as first argument to check functions
2010-10-25 bulwahn changing test parameters in examples to get to a result within the global timelimit
2010-10-25 bulwahn adding a global fixed timeout to quickcheck
2010-10-25 bulwahn adding a global time limit to the values command
2010-10-25 wenzelm explicit message_output thread, with flushing after timeout, ensure atomic user-operations without the danger of IO Interrupt;
2010-10-25 wenzelm more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
2010-10-25 wenzelm renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
2010-10-25 wenzelm explicitly qualify type Output.output, which is a slightly odd internal feature;
2010-10-25 wenzelm export main ML entry by default;
2010-10-25 wenzelm observe Isabelle/ML coding standards;
2010-10-25 wenzelm merged
2010-10-25 wenzelm significantly improved Isabelle/Isar implementation manual;
2010-10-25 wenzelm misc tuning;
2010-10-25 wenzelm removed some remains of Output.debug (follow-up to fce2202892c4);
2010-10-25 wenzelm recovered some odd two-dimensional layout;
2010-10-25 haftmann merged
2010-10-25 haftmann dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
2010-10-25 haftmann moved sledgehammer to Plain; tuned dependencies
2010-10-25 haftmann CONTRIBUTORS
2010-10-25 blanchet merge
2010-10-25 blanchet merged
2010-10-25 blanchet updated keywords
2010-10-25 blanchet introduced manual version of "Auto Solve" as "solve_direct"
2010-10-25 blanchet make "sledgehammer_params" work on single-threaded platforms
2010-10-22 blanchet tuning
2010-10-22 blanchet handle timeouts (to prevent failure from other threads);
2010-10-25 haftmann update keywords
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip