dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document

added note on countable types

simulate more closely the behaviour of the tactic

merged

merged

merged

dropped debug message

more precise text

SMLdummy target

fixed typos

moved theory Quicksort from Library/ to ex/

Theory Multiset provides stable quicksort implementation of sort_key.

added code lemmas for stable parametrized quicksort

tuned proof

moved file in makefile to reflect actual dependencies

give E one more second, to prevent cases where it finds a proof but has no time to print it

use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages; updated docs

don't be overly verbose in Sledgehammer's minimizer

standardize on seconds for Nitpick and Sledgehammer timeouts

cleaned up

added property "tooltip-margin";

clarified tooltips: message output by default, extra info via control/command;

warn in correlation with report -- avoid spurious message duplicates;

tuned;

feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);

merged

updated SMT certificates

standardize timeout value based on reals

merged

merged

change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'

merged

renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun

renamed lemma cont2cont_Rep_CFun to cont2cont_APP

simplify proof of typedef_cont_Abs

rename constant trifte to tr_case

add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t'

make syntax of continuous if-then-else consistent with HOL if-then-else

rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff

polyml_as_definition does not require explicit dependencies on external ML files

explicit warning about opaque signature matching -- saves extra paragraph in implementation manual;

discontinued obsolete function sys_error and exception SYS_ERROR;

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

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

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