even more robust \isaspacing;

simplified Name.variant -- discontinued builtin fold_map;

some attempts at robust \isaspacing so that \isa{...} can be used in section headings etc. (need to avoid `\? for some reason);

discontinued Name.variant to emphasize that this is old-style / indirect;

prefer new-style Name.invents;

more tight name invention -- avoiding old functions;

\frenchspacing for formal isabelle style avoids extra space in situations like ``@{text "?"}'' followed by plain text;

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"