simplified method syntax of "smt", full normalization of binders, corrected translation of patterns into intermediate format, ignore empty lines in Z3 output

merged

adjusted import to changed HOL theory graph

moved theory Divides after theory Nat_Numeral; tuned some proof texts

proper nested quotes; give up unposixly < <(...) for now -- it needs to be exportable through the global environment (e.g. via make or sh);

components: ensure that the last line is read, even if it lacks EOL;

updated Isar.goal;

renamed raw Proof.get_goal to Proof.raw_goal;

back to Proof.raw_goal;

renamed Proof.flat_goal to Proof.simple_goal;

Isar.goal: Proof.simple_goal, not raw version;

replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;

provide SpecParse.constdecl/constdef, e.g. for quotient_definition;

slightly more robust error message;

tuned;

merged

merged

misc tuning;

let naming transform binding beforehand -- covering only the "conceal" flag for now; export LocalTheory.standard_morphism;

tuned;

simplified default binding; conceal internal bindings;

conceal internal bindings;

Drule.store: proper binding; conceal internal bindings;

added restore_naming;

load Product_Type before Nat; dropped junk

moved lemmas for dvd on nat to theories Nat and Power

Probability tweaks

merged

New theory Probability, which contains a development of measure theory

merged

New theory SupInf of the supremum and infimum operators for sets of reals.

eliminated hard tabulators, guessing at each author's individual tab-width;

tuned initial session setup;

merged

proper headers;

reactivated sun-poly, as parallel test;

merged

merged

merged

merged

merged

disabled test case for predicate compiler due to an problem in the inductive package

added examples for quickcheck prototype

adding a prototype of a counter-example generator based on the predicate compiler to HOL/ex

adding test case for inlining of predicate compiler

hiding randompred definitions

changes to example file

print retrieved specification when printing intermediate results

added option show_modes to predicate compiler

including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck

removed unused file smt_builtin.ML, made negative pattern polymorphic (similar to positve pattern)

included description for sledgehammer options in Mirabelle script

measure runtime of ATPs only if requested

eliminated some old folds;

eliminated some old folds;

Datatype.read_typ: standard argument order; eliminated some old folds;

normalized basic type abbreviations;

misc tuning and simplification;

merged

merged

merged

merged

tuned

tuned

dropped obsolete comment

added implode and explode

added friendly error message when Kodkodi is not available

internal renaming in Nitpick and fixed Kodkodi invokation on Linux; renamed Nitpick's ML structures from NitpickXxx to Nitpick_Xxx and added KODKODI_JAVA_LIBRARY_PATH to LD_LIBRARY_PATH before invoking Kodkodi

merged

merged

made Nitpick aware of the KODKODI_JAVA_LIBRARY_PATH, for detecting and properly invoking JNI-based SAT solvers

more thread-safe access to global refs;

avoid structure alias;

comment;

non-critical output -- ship message in one piece;

ProofContext.setmp_verbose_CRITICAL;

non-critical atomic accesses;

critical comments;

tuned;

SimpleThread.fork: uniform handling of outermost Interrupt, which is not an error and should not produce exception trace;

max_threads_value: eliminated tested_platform -- Poly/ML 5.3 fully supports linux, darwin, solaris, cygwin;

lemma converse_inv_image

authentic constants; moved "acyclic" further down

point-free characterization of well-foundedness

replaced (outdated) comments by explicit statements

reactivated test on sunbroy2 -- with full proof parallelism (requires Poly/ML-SVN-921);

forget old some old option stuff from NJ -- superceded by material in Pure/General/basics.ML;

tuned;

added nitpick manual here;

recovered sort indentation for "sort position", as documented in the file; more precise dependencies -- HOL-Multivariate_Analysis produces an image; tuned;

tuned white space;

merged

merged

avoid upto if not needed

conceal quickcheck generators

merged