Remove unnecessary premise of mult1_union

adapting HOL-Mutabelle to changes in quickcheck

NEWS

changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context

updating documentation on quickcheck in the Isar reference

merged

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

tuned messages;

discontinued obsolete ML antiquotation @{theory_ref};

tuned;

moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref; tuned;

type attribute is derived concept outside the kernel;

preserve original source position of exn;

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;

use Exn.interruptible_capture to keep user-code interruptible (Exn.capture not immediately followed by Exn.release here);

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;

eliminated dead code;

tuned white-space;

merged

added lemmas about listrel(1)

tuned;

merged

support non-identifier-like fact names in Sledgehammer (e.g., "my lemma") by quoting them

merged

clear identification

clear identification; thread "Auto S/H" (vs. manual S/H) setting through SMT

clear identification

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)

do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"

generalize to handle any prover (not just E)

merged

make domain package work with non-cpo argument types

make op -->> infixr, to match op --->

use Named_Thms instead of Theory_Data for some domain package theorems

change types of ML commands add_domain, add_new_domain to take 'sort' instead of 'string option'

use Term.add_tfreesT

rename case combinators generated by domain package to 'foo_case' instead of 'foo_when'

rename constant 'one_when' to 'one_case'

merged

sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas

regenerated keyword file

made SML/NJ happy

adapted SMT solver error handling to reflect latest changes in "SMT_Solver"

better list of irrelevant SMT constants

if "debug" is on, print list of relevant facts (poweruser request); internal renaming

standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module

"Nitpick" -> "Sledgehammer"; reparagraphing

merge

merged

remove needless context argument; prefer "Proof.context_of" to "#context o Proof.goal", since it considers any "using [[...]]"

use proper context

trace assumptions before giving them to the SMT solver

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

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

include ATP in theory List -- avoid theory edge by-passing the prominent list theory

fixed typo

merged

merged

put theorems added using "add:" at the beginning of the list returned by the relevance filter, so that they don't get truncated away

tuning