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;

Name_Space.naming: maintain group and theory_name as well; tuned;

export is_concealed; tuned;

merge_list: no exception DUP here;

merged

more uniform ISABELLE_USEDIR_OPTIONS;

make SML/NJ happy;

conceal consts via name space, not tags;

allow name space entries to be "concealed" -- via binding/naming/local_theory;

switch to polyml-5.2.1 to see if it impacts performance;

merged

Multivariate polynomials library over fields

A theory of polynomials based on lists

Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)

merged

further changes due to the previous merge in the predicate compiler

merge -- imported from bulwahn d759e2728188;

removed tuple functions from the predicate compiler

improving the compilation with higher-order arguments in the predicate compiler

now the predicate compilere handles the predicate without introduction rules better as before

removed dead code; added examples

removed obsolete GeneratorPrem; clean-up after modularization; tuned

modularized the compilation in the predicate compiler

adapted parser for options in the predicate compiler

modifying the depth-limited compilation to be sound, but now throws an error undefined in case of hitting the depth limit in an negative context; cleaning up the examples

cleaning the signature of the predicate compiler core; renaming signature and structures to uniform long names

added skip_proof option; playing with compilation of depth-limited predicates

reinvestigating the compilation of the random computation in the predicate compiler

added option to generate random values to values command in the predicate compiler

commented out the random generator compilation in the example file

added option to execute depth-limited computations for the values command in the predicate compiler

renamed functions from sizelim to more natural name depth_limited for compilation of depth-limited search in the predicate compiler

simplified and improved compilation of depth-limited search in the predicate compiler

moved argument expected_modes into options; improved mode check to only check mode of the named predicate

removed unnecessary argument rpred in code_pred function

added option show_mode_inference; added splitting of conjunctions in expand_tuples

changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned

further cleaning up

added option show_proof_trace

importing of polymorphic introduction rules with different schematic variable names

added option show_intermediate_results

continued cleaning up; moved tuple expanding to core

cleaned up debugging messages; added options to code_pred command

added first support for higher-order function translation

added to process higher-order arguments by adding new constants

cleaned up

added theory with alternative definitions for the predicate compiler; cleaned up examples

importing theorems correctly causes problems with mutual recursive predicates in the predicate compiler; must be discussed with Stefan first

higher-order arguments in different rules are fixed to one name in the predicate compiler

changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned

changed proof method to handle widen predicate in JinjaThreads

added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex

processing of tuples in introduction rules

added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions

developing an executable the operator