fix example to reflect change in function signature

make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled

added gotcha to Nitpick manual regarding nonstandard models of "nat"

improve Nitpick's "Datatypes" rendering for elements containing cycles

don't destroy "Suc" in Nitpick and fix logic of Kodkod filtering (accidentally flipped in previous change)

merged

added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested

merge

reintroduce structural induction hint in Nitpick

merge

synchronize Nitpick's wellfoundedness formulas caching

more work on Nitpick's support for nonstandard models + fix in model reconstruction

redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)

minor fixes to Nitpick

various cosmetic changes to Nitpick

merged

fix more looping simp rules

remove $ from all HOLCF files

Renamed Multivariate-Analysis/Integration to Multivariate-Analysis/Integration_MV to avoid name clash with Integration.

Added integration to Multivariate-Analysis (upto FTC)

Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.

fix looping simp rule

fix warnings about duplicate simp rules

fix warnings about duplicate simp rules

add theory HOLCF/ex/Strict_Fun.thy

tuned primrec signature: return definienda

merged

example for executable choice

added simple theory about discrete summation

giving up sunbroy2;

merged

a draft for an example how to turn specifications involving choice executable

added lemma map_of_map_restrict; generalized lemma dom_const

adjusted to changes in theory Mapping

more close integration with theory Map

mappings implemented by association lists

merged

updated SMT certificates

include solver arguments as comments in SMT problem files (to distinguish different results from the same problem when caching results)

updated SMT certificates

added Cache_IO: cache for output of external tools, changed SMT solver interface to use Cache_IO

Rename transp to transpose in HOL-Multivariate_Analysis. (by himmelma)

simplified/clarified record print translations;

eliminated camel case;

tuned;

simplified/clarified record translations;

moved generic update_name to Pure syntax -- not specific to HOL/record;

tuned;

comment;

conceal internal record definitions;

simplified meaning of ProofContext.verbose; eliminated strange ProofContext.setmp_verbose_CRITICAL; less confusing printing of (cumulative) unnamed facts;

refrain from using @{const_name} in syntax translations;

misc tuning and simplification;

refined and exported record_info;

modernized structures;

modernized signature -- proper binding; misc tuning;

tuned errors; tuned;

Typedef.the_info;

formal markup of constants; misc tuning;

tuned document;

eliminated old fold;

renamed InfixName to Infix etc.;

discontinued unnamed infix syntax;

eliminated unnamed infixes;