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

merged

make Nitpick compile again

merged

be somewhat more liberal in Nitpick about which types may occur in formulas

make the Nitpick examples work again

updated keyword files to include "nitpick" and "nitpick_params"

continuation of Nitpick's integration into Isabelle; added examples, and integrated non-Main theories better.

updated Nitpick documentation to remove weird default for "overlord"

updated Nitpick manual to reflect the latest Stand der Dinge

merged

wrap line correctly in Nitpick documentation

added Nitpick's theory and ML files to Isabelle/HOL; the examples and the documentation are on their way.

Added Nitpick manual.

merged

Added Pattern.thy to Nominal/Examples.

merged

tuned

added SML_Quickcheck import

tuned code setup for primitive boolean connectors

legacy warnings for old-style term styles

removed unnecessary NameSpace prefix;

misc tuning and updates;

merged

implicit default is 4 cores -- more cost-effective;

deleted junk;

more precise dependencies, notably for HOL-Multivariate_Analysis;

re-moved theory Fin_Fun to AFP

merged

distinguished session for multivariate analysis

adjusted to changes in corresponding ML code

eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;

maintain theory name via name space, not tags; AxClass.thynames_of_arity: explicit theory name, not tags;

name space groups are identified by serial, not serial_string;

maintain group via name space, not tags; tuned;

LocalTheory.naming_of;

begin_theory: set theory_name here;

maintain group via name space, not tags;

maintain proper Name_Space.naming, with conceal and set_group; maintain group via name space, not tags; tuned signature; tuned;

more direct access to naming; tuned signature;