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

merged

consider base sorts of superclasses simultaneously during processing of class specification -- avoids clash of different base sorts

more general treatment of type argument in code certificates for operations on abstract types

partial_function is a declaration command

merged

proper error handling for SMT solvers in Sledgehammer

NEWS

merge

integrated "smt" proof method with Sledgehammer

fixed confusion introduced in 008dc2d2c395

merged

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

merged

tuned

merged

use partial_function instead of MREC combinator; curried rev'

added Heap monad instance of partial_function package

added Spec_Rule declaration to partial_function

basic documentation for command partial_function

remove outdated "(otherwise)" syntax from manual

declare recursive equation as ".simps", in accordance with other packages

merged

dropped accidental doubled computation

optionally force the remote version of an SMT solver to be executed

tuned

added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)

changed SMT configuration options; updated SMT certificates

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

keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs

merged

merge

clearer error messages

renaming

back again to non-Apple font rendering (cf. 4977324373f2);

dock isabelle-session at bottom (again, cf. 37bdc2220cf8) to ensure that controls are fully visible;

disable broken popups for now;

tuned;

do not handle arbitrary exceptions;

merged

Code_Runtime.trace

proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};