no polymorphic "var"s

merged

adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples

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

tuned

accomodate for scope of "as" binding in ML

tuned code

datatype classes are abstract

avoid deprecation

robustified metis proof

modernized abel_cancel simproc setup

keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup

diff_eq_diff_less_eq' replaces diff_eq_diff_less_eq

diff_minus subsumes diff_def

tuned whitespace

dropped essentially ineffective tuning

discontinued pretending that abel_cancel is logic-independent; cleaned up junk

merged

merged

distinguish different classes of const syntax

Scala: subtle difference in printing strings vs. complex mixfix syntax

check code generation for Scala

dropped superfluous prefixes

optional break

consolidate const_syntax naming

recovered benchmarks, which are not tested automatically;

reactivate SML/NJ test on macbroy28, while macbroy23 is unavailable;

eliminated old time_use/time_use_thy variants -- timing is implicitly controlled via Output.timing; misc tuning and simplification;

moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway;