tuned;

NEWS

correcting import theory of examples

fixing code generation test

removing char setup

removing unneccessary manual instantiations and dead definitions; hiding more constants and facts

adding a nicer error message for quickcheck_narrowing; hiding fact empty_def

adding narrowing engine for existentials

adapting Quickcheck_Narrowing: adding setup for characters; correcting import statement

adding theory Quickcheck_Narrowing to HOL-Main image

adapting IsaMakefile

moving Quickcheck_Narrowing from Library to base directory

compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators

local simp rule in List_Cset

tuning

compile

cleaner fact freshening, which also works in corner cases, e.g. if two backquoted facts have the same name (but have different variable indices)

added a really fully typed translation as a fallback for Metis, in rare cases where Metis correctly proves a theorem but has type-unsound steps in it (which is likelier to happen with some of the lighter translations)

improve sort inference in Metis proofs -- in some rare cases Metis steals Isabelle's variable names and the sorts must then be inferred as well

removed needless function that duplicated standard functionality, with a little unnecessary twist

removed more dead code

be a bit more liberal with respect to the universal sort -- it sometimes help

renamed "untyped_aconv" to distinguish it clearly from the standard "aconv_untyped"

merged

avoid duplicate facts, which confuse the minimizer output

pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types

restore comment about subtle issue

made "query" type systes a bit more sound -- local facts, e.g. the negated conjecture, may make invalid the infinity check, e.g. if we are proving that there exists two values of an infinite type, we can use the negated conjecture that there is only one value to derive unsound proofs unless the type is properly encoded

don't launch the automatic minimizer for zero facts

don't generate unsound proof error for missing proofs