try_param_tac: plain user error appears more appropriate;

replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;

eliminated dead code;

more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR; proper signature constraint;

removed assumption

more on naming tactics;

merged

merged

tuned proof

tuned proof

tuned lemma proposition of properties_for_sort_key

lemmas sorted_map_same, sorted_same

lemmas multiset_of_filter, sort_key_by_quicksort

more on "Time" in Isabelle/ML;

simplified some time constants;

added convenience operation seconds: real -> time;

avoid catch-all exception handling;

eliminated fragile catch-all pattern, based on educated guess about the intended exception;

Attribute map_function -> coercion_map; tuned;

syntax category "real" subsumes plain "int";

merged

Plus -> Sum_Type.Plus

Minor reformat.

support for real valued preferences;

support for real valued configuration options;

support for floating-point tokens in outer syntax (coinciding with inner syntax version);

merged

added rule let_mono

CONTRIBUTORS;

more sharing of operations, without aliases;

simplified data lookup;

export declarations by default, to allow other ML packages by-pass concrete syntax; proper Args parsing for attribute syntax (required for proper treatment of morphisms when declarations are moved between contexts); tuned;

proper signature constraint for ML structure; explicit theory setup, which is customary outside Pure; formal @{binding} instead of Binding.name;

proper header; tuned whitespace;

Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).

updated SMT certificates

eta-expand built-in constants; also rewrite partially applied natural number terms

optionally drop assumptions which cannot be preprocessed

added crafted list of SMT built-in constants

clarified error message

tuned

introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list

merged

added listrel1

hide Sum_Type.Plus

merged

added user aliasses (still unclear how to specify names with whitespace contained)

merged

tuned structure of theory

remove term_of equations for Heap type explicitly

no need for setting up the kodkodi environment since Kodkodi 1.2.9

fixed order of quantifier instantiation in new Skolemizer

restructure Skolemization code slightly

ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)

more work on new Skolemizer without Hilbert_Choice

fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)

prevent type errors because of inconsistent skolem Var types by giving fresh indices to Skolems

make handling of parameters more robust, by querying the goal

actually pass "verbose" argument

eliminated obsolete \_ escape;

eliminated obsolete \_ escapes in rail environments;

proper markup of formal text;

merged

hide_const various constants, in particular to avoid ugly qualifiers in HOLCF

reverted e31e3f0071d4 because "foo.bar(5)" (with quotes) is wrong

merged

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

merged

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