added new proof redirection code

SPASS is incomplete because of the -Splits and -FullRed options, not just because of -SOS=1 -- don't pretend the opposite

make sure that all symbols are declared in untyped SPASS DFG output (broken since 3b8606fba2dd)

NEWS

correcting dependencies after renaming

tuned header after renaming

moving AList theory to AList_Impl to make space for the association lists with invariant

merged

adding map_entry to AList theory

adding map_default to AList theory

fixed typo in theorem name in AList theory

adding code attribute to enable evaluation of equality on multisets

merged

updated Sledgehammer/SMT docs

tuned signature;

eliminated dead code;

some full isatest runs, which include benchmark targets;

more visible benchmarks; uniform IsaMakefile target "full" to cover such extra sessions;

fixed Nitpick definition of "<" on "real"s

replace 'lemmas' with 'lemma'

merged

more simp rules for sbintrunc

add simp rules for sbintrunc applied to numerals

replace many uses of 'lemmas' with explicit 'lemma'

add lemma bin_nth_zero

add simp rules for bintrunc applied to numerals

add simp rules for bin_rest and bin_last applied to numerals

add simp rules for bin_sign applied to numerals

add simp rules for BIT applied to numerals

declare BIT_eq_iff [iff]; remove unneeded lemmas

towards removing BIT_simps from the simpset

type signature for bin_sign

remove some unwanted numeral-representation-specific simp rules

remove redundant lemmas

reorder some definitions and proofs, in preparation for new numeral representation

merged

added lemmas

added concrete syntax

'datatype' specifications allow explicit sort constraints; tuned signatures;

do not open ML structures;

tuned;

removed dead code;

comment;

connect while_option with lfp

lemmas about Kleene iteration

merged

avoid multiple type decls in TFF (improves on cef82dc1462d)

added missing quantifier

remove needless declaration in TFF1 problems

correctly declare implicit TFF1 types that appear first as type arguments with "$tType" and not "$i

modernized specifications;

support phantom types as quotient types

merged

merged

tuned

datatype dtyp with explicit sort information; tuned messages;

tuned;

updated generated file;

tuned quickcheck's response

hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;

merged

replace more uses of 'lemmas' with explicit 'lemma'; replace uses of 'simplified' attribute with 'unfolded'; remove unused intermediate lemmas.

Add Quotient_Rat: an example of using the quotient package with partial equivalence relations, defining rational numbers.

fix spelling

fix spelling

added IMP/Live_True.thy

replace many uses of 'lemmas' with 'lemma'; remove many unused intermediate lemmas.

prove class instances without extra lemmas

finite class instance for word type; remove unused lemmas

remove unused lemmas

generalize some lemmas

merged

tidied Word.thy; put attributes directly on lemmas instead of using 'declare'; replace various 'lemmas' commands with ordinary 'lemma'.

remove redundant lemma word_diff_minus

remove some duplicate lemmas, simplify some proofs

Quotient_Info stores only relation maps

hiding definitional facts in Quickcheck; introducing catch_match more honestly

added dependencies

added an example file with lifting of constants with contravariant and co/contravariant types

merged

make ctxt the first parameter

context/theory parametres tuned

maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types

add induction rule for list_all2

deactivating quickcheck_narrowing if Efficient_Nat theory is loaded

tuned quickcheck's response

more systematic lemma name

adding examples for quickcheck narrowing about partial functions

removing special code generator setup for hd and last function because this causes problems with quickcheck narrowing as the Haskell Prelude functions throw errors that cannot be caught instead of PatternFail exceptions

HOLCF/ex/Letrec.thy: keep class 'domain' as default sort

more error checking for fixrec

reinstate old functions cfst and csnd as abbreviations

merged

tuned

merged

added a specific tactic and method that deal with partial equivalence relations

use same order of facts for preplay as for actual reconstruction -- Metis sometimes exhibits very different timings depending on the order of the facts

avoid multiple TFF1 declarations

updated TFF1 support

updated Metis to 20110926 version

remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space

remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead

add cancellation simprocs for type enat

tuned

increasing quickcheck's timeout in the example theory to avoid failures on the testing infrastructure

tuned proofs

added lemmas

tuned proof

real is better supported than real_of_nat, use it in the nat => ereal coercion

merged

the note about morphisms moved in the description part

updating documentation about quiet and verbose options in quickcheck

making the default behaviour of quickcheck a little bit less verbose; adapting quickcheck examples

adding verbose configuration to quickcheck

random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument

the reporting random testing also returns if the counterexample is genuine or potentially spurious

exhaustive returns if a counterexample is genuine or potentially spurious in the presence of assumptions more correctly

inverted flag potential to genuine_only in the quickcheck narrowing Haskell code

NEWS

documenting the genuine_only option in quickcheck;