do a better job at Skolemizing in Nitpick, for TPTP FOF

revert code that was submitted by mistake

renamings + only need second component of name pool to reconstruct proofs

rename "classrel" to "class_rel"

rename "combtyp" constructors

renamed "Literal" to "FOLLiteral"

renamed "HOLClause" to "FOLClause" -- it's really a FOL clause with combinators

merged

fixing quickcheck invocation in HOL-Mirabelle

hiding constants in Quickcheck_Types

adding a type for flat complete lattice to Quickcheck_Types

added new theories to IsaMakefile and ROOT.ML

adding Quickcheck examples for other quickcheck default types

adding Library theory for other quickcheck default types

removing obsolete ID in Quickcheck_Examples

correcting wellsortedness check and improving error message

using multiple default types in quickcheck

correcting merging of default_types

reordering quickcheck signature; exporting test_params and inspection function

changed default types to a list of types; extended quickcheck parameters to be a list of values to parse a list of default types

putting proof in the right context; adding if rewriting; tuned

load_thy: parallel parsing of units, which consist of statement/proof each;

eliminated some unreferenced identifiers;

tuned;

tuned comments;

replaced Source.of_list_limited by slightly more economic Source.of_string_limited;

deps_thy/load_thy: store compact text to reduce space by factor 12;

make SML/NJ happy, by adhoc type-constraints;

recovered benchmarks, which are not tested automatically;

made SML/NJ happy;

merged

abstract visualization of locale ingredients; all_locales yields proper locale identifiers