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