2010-10-29 wenzelm 2010-10-29 proper markup of formal text;
2010-10-29 wenzelm 2010-10-29 merged
2010-10-29 krauss 2010-10-29 hide_const various constants, in particular to avoid ugly qualifiers in HOLCF
2010-10-29 blanchet 2010-10-29 reverted e31e3f0071d4 because "foo.bar(5)" (with quotes) is wrong
2010-10-29 Lars Noschinski 2010-10-29 merged
2010-09-22 Lars Noschinski 2010-09-22 Remove unnecessary premise of mult1_union
2010-10-29 bulwahn 2010-10-29 adapting HOL-Mutabelle to changes in quickcheck
2010-10-29 bulwahn 2010-10-29 NEWS
2010-10-29 bulwahn 2010-10-29 changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context
2010-10-29 bulwahn 2010-10-29 updating documentation on quickcheck in the Isar reference
2010-10-28 bulwahn 2010-10-28 merged
2010-10-28 bulwahn 2010-10-28 adding a simple check to only run with a SWI-Prolog version known to work * * * taking the isabelle platform into account when finding the prolog system
2010-10-28 wenzelm 2010-10-28 tuned messages;
2010-10-28 wenzelm 2010-10-28 discontinued obsolete ML antiquotation @{theory_ref};
2010-10-28 wenzelm 2010-10-28 tuned;
2010-10-28 wenzelm 2010-10-28 moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref; tuned;
2010-10-28 wenzelm 2010-10-28 type attribute is derived concept outside the kernel;
2010-10-28 wenzelm 2010-10-28 preserve original source position of exn;
2010-10-28 wenzelm 2010-10-28 handle Type.TYPE_MATCH, not arbitrary exceptions via MATCH_TYPE variable; clarified handle/raise wrt. Quotient_Info.NotFound -- avoid fragile unqualified NotFound depending on "open" scope; added helpful comments;
2010-10-28 wenzelm 2010-10-28 use Exn.interruptible_capture to keep user-code interruptible (Exn.capture not immediately followed by Exn.release here);
2010-10-28 wenzelm 2010-10-28 added Exn.interruptible_capture, which reraises interrupts as required by user-code (when Exn.capture is not immediately followed by Exn.release); refined Exn.is_interrupt: detect nested IO Interrupts; generalized Exn.map_result; more precise dependencies;
2010-10-28 wenzelm 2010-10-28 eliminated dead code;
2010-10-28 wenzelm 2010-10-28 tuned white-space;
2010-10-28 nipkow 2010-10-28 merged
2010-10-28 nipkow 2010-10-28 added lemmas about listrel(1)
2010-10-28 wenzelm 2010-10-28 tuned;
2010-10-28 wenzelm 2010-10-28 merged
2010-10-28 blanchet 2010-10-28 support non-identifier-like fact names in Sledgehammer (e.g., "my lemma") by quoting them
2010-10-28 blanchet 2010-10-28 merged
2010-10-28 blanchet 2010-10-28 clear identification
2010-10-28 blanchet 2010-10-28 clear identification; thread "Auto S/H" (vs. manual S/H) setting through SMT
2010-10-28 blanchet 2010-10-28 clear identification
2010-10-27 blanchet 2010-10-27 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 blanchet 2010-10-27 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 blanchet 2010-10-27 generalize to handle any prover (not just E)
2010-10-27 huffman 2010-10-27 merged
2010-10-27 huffman 2010-10-27 make domain package work with non-cpo argument types
2010-10-27 huffman 2010-10-27 make op -->> infixr, to match op --->
2010-10-26 huffman 2010-10-26 use Named_Thms instead of Theory_Data for some domain package theorems
2010-10-26 huffman 2010-10-26 change types of ML commands add_domain, add_new_domain to take 'sort' instead of 'string option'
2010-10-26 huffman 2010-10-26 use Term.add_tfreesT
2010-10-24 huffman 2010-10-24 rename case combinators generated by domain package to 'foo_case' instead of 'foo_when'
2010-10-24 huffman 2010-10-24 rename constant 'one_when' to 'one_case'
2010-10-27 haftmann 2010-10-27 merged
2010-10-27 haftmann 2010-10-27 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 krauss 2010-10-27 regenerated keyword file
2010-10-27 boehmes 2010-10-27 made SML/NJ happy
2010-10-26 blanchet 2010-10-26 adapted SMT solver error handling to reflect latest changes in "SMT_Solver"
2010-10-26 blanchet 2010-10-26 better list of irrelevant SMT constants
2010-10-26 blanchet 2010-10-26 if "debug" is on, print list of relevant facts (poweruser request); internal renaming
2010-10-26 blanchet 2010-10-26 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
2010-10-26 blanchet 2010-10-26 "Nitpick" -> "Sledgehammer"; reparagraphing
2010-10-26 blanchet 2010-10-26 merge
2010-10-26 blanchet 2010-10-26 merged
2010-10-26 blanchet 2010-10-26 remove needless context argument; prefer "Proof.context_of" to "#context o Proof.goal", since it considers any "using [[...]]"
2010-10-26 boehmes 2010-10-26 use proper context
2010-10-26 boehmes 2010-10-26 trace assumptions before giving them to the SMT solver
2010-10-26 boehmes 2010-10-26 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 boehmes 2010-10-26 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 haftmann 2010-10-26 include ATP in theory List -- avoid theory edge by-passing the prominent list theory