isabelle: Graph

merged
2010-10-28, by nipkow
added lemmas about listrel(1)
2010-10-28, by nipkow
tuned;
2010-10-28, by wenzelm
merged
2010-10-28, by wenzelm
support non-identifier-like fact names in Sledgehammer (e.g., "my lemma") by quoting them
2010-10-28, by blanchet
merged
2010-10-28, by blanchet
clear identification
2010-10-28, by blanchet
clear identification;
2010-10-28, by blanchet
clear identification
2010-10-28, by blanchet
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
2010-10-27, by blanchet
do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
2010-10-27, by blanchet
generalize to handle any prover (not just E)
2010-10-27, by blanchet
merged
2010-10-27, by huffman
make domain package work with non-cpo argument types
2010-10-27, by huffman
make op -->> infixr, to match op --->
2010-10-27, by huffman
use Named_Thms instead of Theory_Data for some domain package theorems
2010-10-26, by huffman
change types of ML commands add_domain, add_new_domain to take 'sort' instead of 'string option'
2010-10-26, by huffman
use Term.add_tfreesT
2010-10-26, by huffman
rename case combinators generated by domain package to 'foo_case' instead of 'foo_when'
2010-10-24, by huffman
rename constant 'one_when' to 'one_case'
2010-10-24, by huffman
merged
2010-10-27, by haftmann
sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
2010-10-27, by haftmann
regenerated keyword file
2010-10-27, by krauss
made SML/NJ happy
2010-10-27, by boehmes
adapted SMT solver error handling to reflect latest changes in "SMT_Solver"
2010-10-26, by blanchet
better list of irrelevant SMT constants
2010-10-26, by blanchet
if "debug" is on, print list of relevant facts (poweruser request);
2010-10-26, by blanchet
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
2010-10-26, by blanchet
"Nitpick" -> "Sledgehammer";
2010-10-26, by blanchet
merge
2010-10-26, by blanchet
merged
2010-10-26, by blanchet
remove needless context argument;
2010-10-26, by blanchet
use proper context
2010-10-26, by boehmes
trace assumptions before giving them to the SMT solver
2010-10-26, by boehmes
capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1
2010-10-26, by boehmes
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
2010-10-26, by boehmes
include ATP in theory List -- avoid theory edge by-passing the prominent list theory
2010-10-26, by haftmann
fixed typo
2010-10-26, by krauss
merged
2010-10-26, by blanchet
merged
2010-10-26, by blanchet
put theorems added using "add:" at the beginning of the list returned by the relevance filter, so that they don't get truncated away
2010-10-26, by blanchet
tuning
2010-10-26, by blanchet
merged
2010-10-26, by haftmann
consider base sorts of superclasses simultaneously during processing of class specification -- avoids clash of different base sorts
2010-10-26, by haftmann
more general treatment of type argument in code certificates for operations on abstract types
2010-10-26, by haftmann
partial_function is a declaration command
2010-10-26, by haftmann
merged
2010-10-26, by blanchet
proper error handling for SMT solvers in Sledgehammer
2010-10-26, by blanchet
NEWS
2010-10-26, by krauss
merge
2010-10-26, by blanchet
integrated "smt" proof method with Sledgehammer
2010-10-26, by blanchet
fixed confusion introduced in 008dc2d2c395
2010-10-26, by krauss
merged
2010-10-26, by blanchet
reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
2010-10-26, by blanchet
merged
2010-10-26, by haftmann
tuned
2010-10-26, by haftmann
merged
2010-10-26, by krauss
use partial_function instead of MREC combinator; curried rev'
2010-10-26, by krauss
added Heap monad instance of partial_function package
2010-10-26, by krauss
added Spec_Rule declaration to partial_function
2010-10-26, by krauss
basic documentation for command partial_function
2010-10-26, by krauss
remove outdated "(otherwise)" syntax from manual
2010-10-26, by krauss
declare recursive equation as ".simps", in accordance with other packages
2010-10-26, by krauss
merged
2010-10-26, by haftmann
dropped accidental doubled computation
2010-10-26, by haftmann
optionally force the remote version of an SMT solver to be executed
2010-10-26, by boehmes
tuned
2010-10-26, by boehmes
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
2010-10-26, by boehmes
changed SMT configuration options; updated SMT certificates
2010-10-26, by 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, by 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, by boehmes
merged
2010-10-26, by blanchet
merge
2010-10-26, by blanchet
clearer error messages
2010-10-26, by blanchet
renaming
2010-10-26, by blanchet
back again to non-Apple font rendering (cf. 4977324373f2);
2010-10-28, by wenzelm
dock isabelle-session at bottom (again, cf. 37bdc2220cf8) to ensure that controls are fully visible;
2010-10-28, by wenzelm
disable broken popups for now;
2010-10-26, by wenzelm
tuned;
2010-10-26, by wenzelm
do not handle arbitrary exceptions;
2010-10-26, by wenzelm
merged
2010-10-26, by wenzelm
Code_Runtime.trace
2010-10-26, by haftmann
proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
2010-10-26, by wenzelm
merged
2010-10-26, by wenzelm
improved English
2010-10-26, by blanchet
whitespace tuning
2010-10-26, by blanchet
no need to encode theorem number twice in skolem names
2010-10-26, by blanchet
tuning
2010-10-26, by blanchet
make SML/NJ happy
2010-10-26, by blanchet
relaxing the filtering condition for getting specifications from Spec_Rules
2010-10-25, by bulwahn
adding new predicate compiler files to the IsaMakefile
2010-10-25, by bulwahn
using mode_eq instead of op = for lookup in the predicate compiler
2010-10-25, by bulwahn
renaming split_modeT' to split_modeT
2010-10-25, by bulwahn
options as first argument to check functions
2010-10-25, by bulwahn
changing test parameters in examples to get to a result within the global timelimit
2010-10-25, by bulwahn
adding a global fixed timeout to quickcheck
2010-10-25, by bulwahn
adding a global time limit to the values command
2010-10-25, by bulwahn
explicit message_output thread, with flushing after timeout, ensure atomic user-operations without the danger of IO Interrupt;
2010-10-25, by wenzelm
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
2010-10-25, by wenzelm
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
2010-10-25, by wenzelm
explicitly qualify type Output.output, which is a slightly odd internal feature;
2010-10-25, by wenzelm
export main ML entry by default;
2010-10-25, by wenzelm
observe Isabelle/ML coding standards;
2010-10-25, by wenzelm
merged
2010-10-25, by wenzelm
significantly improved Isabelle/Isar implementation manual;
2010-10-25, by wenzelm
misc tuning;
2010-10-25, by wenzelm
removed some remains of Output.debug (follow-up to fce2202892c4);
2010-10-25, by wenzelm
recovered some odd two-dimensional layout;
2010-10-25, by wenzelm
merged
2010-10-25, by haftmann
dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
2010-10-25, by haftmann
moved sledgehammer to Plain; tuned dependencies
2010-10-25, by haftmann
CONTRIBUTORS
2010-10-25, by haftmann
merge
2010-10-25, by blanchet
merged
2010-10-25, by blanchet
updated keywords
2010-10-25, by blanchet
introduced manual version of "Auto Solve" as "solve_direct"
2010-10-25, by blanchet
make "sledgehammer_params" work on single-threaded platforms
2010-10-25, by blanchet
tuning
2010-10-22, by blanchet
handle timeouts (to prevent failure from other threads);
2010-10-22, by blanchet
update keywords
2010-10-25, by haftmann