remove " s" suffix since seconds are now implicit

ignore facts with only theory constants in them

cosmetics

use the SMT integration's official list of built-ins

added class relation group_add < cancel_semigroup_add

merged

changing timeout to real value; handling Interrupt and Timeout more like nitpick does

added two lemmas about injectivity of concat to the list theory

adding documentation of some quickcheck options

merged

Code.check_const etc.: reject too specific types

corrected quoting

added lemma length_alloc

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

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

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};

merged

improved English

whitespace tuning

no need to encode theorem number twice in skolem names

tuning

make SML/NJ happy

relaxing the filtering condition for getting specifications from Spec_Rules

adding new predicate compiler files to the IsaMakefile

using mode_eq instead of op = for lookup in the predicate compiler

renaming split_modeT' to split_modeT

options as first argument to check functions

changing test parameters in examples to get to a result within the global timelimit

adding a global fixed timeout to quickcheck

adding a global time limit to the values command

explicit message_output thread, with flushing after timeout, ensure atomic user-operations without the danger of IO Interrupt; eliminated auto_flush threads -- use plain line buffering for stdout/stderr; tuned;

more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);

renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;

explicitly qualify type Output.output, which is a slightly odd internal feature;

export main ML entry by default; observe elisp format for preferences; clarified command setup;

observe Isabelle/ML coding standards;

merged

significantly improved Isabelle/Isar implementation manual;

misc tuning;

removed some remains of Output.debug (follow-up to fce2202892c4);

recovered some odd two-dimensional layout;

merged

dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps

moved sledgehammer to Plain; tuned dependencies

CONTRIBUTORS

merge

merged

updated keywords

introduced manual version of "Auto Solve" as "solve_direct"

make "sledgehammer_params" work on single-threaded platforms

tuning

handle timeouts (to prevent failure from other threads); removed needless functions; added "metis" to the mix

update keywords

some partial_function examples

added ML antiquotation @{assert};

updated keywords;

integrated partial_function into HOL-Plain

first version of partial_function package

Complete_Partial_Order.thy: complete partial orders over arbitrary chains, with fixpoint theorem

merged

splitting Hotel Key card example into specification and the two tests for counter example generation

adding generator quickcheck

restructuring values command and adding generator compilation

moving general functions from core_data to predicate_compile_aux

updating to new notation in commented examples

merged

use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum

remove legacy comp_dbind option from domain package

change fixrec parser to not accept theorem names with (unchecked) option

tuned

rename lemma surjective_pairing_Sprod2 to spair_sfst_ssnd

add lemma strict3

do proofs using Rep_Sprod_simps, Rep_Ssum_simps; remove unused lemmas

make discrete_cpo a subclass of chfin; remove chfin instances for fun, cfun

direct instantiation unit :: discrete_cpo

remove finite_po class

simplify proofs about flift; remove unneeded lemmas

simplify proof

minimize imports

add type annotation to avoid warning

simplify some proofs, convert to Isar style

rename lemma spair_lemma to spair_Sprod

pcpodef (open) 'a lift

remove intro! attribute from {sinl,sinr}_defined

simplify proofs of ssumE, sprodE

merged

renamed nat_number

nat_number -> eval_nat_numeral

some cleanup in Function_Lib

merged

compile

added SMT solver to Sledgehammer docs

more robust handling of "remote_" vs. non-"remote_" provers

generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)

replaced references with proper record that's threaded through

fixed signature of "is_smt_solver_installed"; renaming

renamed modules

renamed files

took out "smt"/"remote_smt" from default ATPs until they are properly implemented

remove more needless code ("run_smt_solvers"); tuning

got rid of duplicate functionality ("run_smt_solver_somehow"); added minimization command to SMT solver message

bring ATPs and SMT solvers more in line with each other

make Sledgehammer minimizer fully work with SMT

generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well

first step in adding support for an SMT backend to Sledgehammer

use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."

cosmetics

relation method: re-check given term with type constraints to avoid unspecific failure if ill-typed -- keep old behaviour for tactic version

Changed section title to please LaTeX.

temporary removed Predicate_Compile_Quickcheck_Examples from tests

adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog

using a signature in core_data and moving some more functions to core_data

splitting large core file into core_data, mode_inference and predicate_compile_proof

added generator_dseq compilation for a sound depth-limited compilation with small value generators

for now safely but unpractically assume no predicate is terminating

adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible

adding option smart_depth_limiting to predicate compiler

merged

introduce function strict :: 'a -> 'b -> 'b, which works like Haskell's seq; use strict instead of strictify in various definitions

add lemma lub_eq_bottom_iff

combine check_and_sort_domain with main function; rewrite much of the error-checking code

constructor arguments with selectors must have pointed types

simplify check_and_sort_domain; more meaningful variable names

replace fixrec 'permissive' mode with per-equation 'unchecked' option

rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML

simplify some proofs; remove some unused lists of lemmas

replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function

eliminate constant 'coerce'; use 'prj oo emb' instead

simplify fixrec pattern match function

simplify some proofs

tuned

added some facts about factorial and dvd, div and mod

removing something that probably slipped into the Quotient_List theory

Quotient package: partial equivalence introduction

reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)

remove dead code

remove old uses of 'simp_tac HOLCF_ss'

merged

remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check

reimplement proof automation for coinduct rules

add functions mk_imp, mk_all

move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code

simplify automation of induct proof

add function mk_adm

rewrite proof automation for finite_ind; get rid of case_UU_tac

put constructor argument specs in constr_info type

avoid using Global_Theory.get_thm

include iso_info as part of constr_info type

remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors

add take_strict_thms field to take_info type

add record type synonym 'constr_info'

add function take_theorems

add type annotation to avoid warning

cleaned up Fun_Cpo.thy; deprecated a few theorem names

edit comments

remove unneeded lemmas Lift_exhaust, Lift_cases

move lemmas from Lift.thy to Cfun.thy

cleaned up Adm.thy

remove unneeded lemmas from Fun_Cpo.thy

remove unused lemmas

reformulate lemma cont2cont_lub and move to Cont.thy

remove unused lemmas cont_fst_snd_D1, cont_fst_snd_D2

new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI

rename Ffun.thy to Fun_Cpo.thy

remove unused constant 'directed'

add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite

merged

prevention of self-referential type environments

FSet: definition changes propagated from Nominal and more use of 'descending' tactic

FSet tuned

FSet: give names to respectfulness theorems, rename list_all2_refl to avoid clash

NEWS

removed output syntax "'a ~=> 'b" for "'a => 'b option"

reactivated

slightly more robust proof

renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)

merged

move all bifinite class instances to Bifinite.thy

rename class 'sfp' to 'bifinite'

move stuff from Algebraic.thy to Bifinite.thy and elsewhere

add lemma typedef_ideal_completion

remove unused lemmas

remove Infinite_Set from ROOT.ML

remove some junk that made it in by accient

"setup" in theory

added "trace_meson" configuration option, replacing old-fashioned reference

added "trace_metis" configuration option, replacing old-fashioned references

do not mention unqualified names, now that 'global' and 'local' are gone

simplified proof

avoid generating several formulas with the same name ("tfrees")

major reorganization/simplification of HOLCF type classes: removed profinite/bifinite classes and approx function; universal domain uses approx_chain locale instead of bifinite class; ideal_completion locale does not use 'take' functions, requires countable basis instead; replaced type 'udom alg_defl' with type 'sfp'; replaced class 'rep' with class 'sfp'; renamed REP('a) to SFP('a);

add lemma finite_deflation_intro

add lemmas finite_deflation_imp_compact, cast_below_cast_iff

move lemmas to Deflation.thy

simplify proofs of powerdomain inequalities

new lemmas about lub

define is_ub predicate using bounded quantifier

minimize theory imports

added lemmas to List_Cpo.thy

new_domain emits proper error message when a constructor argument type does not have sort 'rep'

move code from "Metis_Tactics" to "Metis_Reconstruct"

merged

qualify "Meson." and "Metis." constants so that the ML files can be reloaded later (e.g. for testing/development)

get rid of function that duplicates existing Pure functionality

remove needless fact

added a few FIXMEs

tuned comments

document latest changes to Meson/Metis/Sledgehammer

remove needless Metis facts

hide one more name

qualify names

hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names

clean up debugging output

factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure

got rid of overkill "meson_choice" attribute; tuning

more explicit name

factor out "Meson_Tactic" from "Meson_Clausify"

tuning

move Metis into Plain

added "Meson" theory to Makefile

update authors

remove Meson from Hilbert_Choice

remove Meson from Sledgehammer

move Meson to Plain

move MESON files together

paramify new skolems just like old ones (cf. reveal_old_skolem_terms)

fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset

correctly handle multiple copies of the same axiom with the same types

put two operations in the right order

reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism

apply "assume_tac" directly on the right assumption, using "rotate_tac" -- this ensures that the desired unifications are performed

instantiate foralls and release exists in the order described by the topological order

reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables

renamed internal function

hack in MESON to make it less likely that variables (e.g. "x") get renamed (e.g. "xa") when resolving

tuned header

tuned

force less agressively

lexicographic_order: replace parallel map with laziness to avoid wasting cycles on proofs that are not needed

removed complicated (and rarely helpful) error reporting

discontinued continuations to simplify control flow; dropped optimization in scnp

use Cache structure instead of passing tables around explicitly

merged

lemmas fold_commute and fold_commute_apply

spelling

adjusted to inductive characterization of sorted

tuned whitespace

turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs

turned distinct and sorted into inductive predicates: yields nice induction principles for free

turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs

some Poly/ML-specific debugging code escaped in the wild -- comment it out

merged

avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime

moved ML_Context.value to Code_Runtime

constant `contents` renamed to `the_elem`

merged

tune whitespace

rename bound variables after skolemizing, if the axiom of choice is available

tuning

rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)

tune bound names

merged

avoid dependency on "int"

make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice

added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice

compute quantifier dependency graph in new skolemizer

tuning

compute substitutions in new skolemizer

encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions

reintroduced code that keeps track of whether the Isabelle and Metis proofs are in sync -- generalized to work with the new skolemizer

encode number of skolem assumptions in them, for more efficient retrieval later

move functions closer to where they're used