merged

tuned isatest settings;

removed unused Theory_Target.begin; Theory_Target.init: removed Locale.intern, which was accidentally introduced in 40b3630b0deb; renamed Theory_Target.context to Theory_Target.context_cmd to emphasize that this involves Locale.intern; tuned;

locale: more precise treatment of naming vs. binding;

Sign.restore_naming -- slightly more robust;

typedef: slightly more precise treatment of binding; tuned;

axclass: more precise treatment of naming vs. binding;

more systematic treatment of qualified names derived from binding;

pretty_full_theory: proper Syntax.init_pretty_global;

made SML/NJ happy (again);

merged

drop code lemma for ordered_keys

more lemmas about sort(_key)

added ordered_keys

isatest: activated HOL-Nitpick_Examples for x86_64-darwin -- should now work with kodkodi-1.2.8;

merged

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;

apply global morphism for theory, instantiation and overloading target; n.b. target morphism and global morphism coincide for theory target

clarifed type

optionally localize assertion labels (based on user-defined offsets) to reduce the effort of label adaptions after changes to the source program

formal markup of constants;

modernized structures;

authentic proof syntax;

tuned import order

tuned comments

merged

merged

change generated lemmas dist_eqs and dist_les to iff-style

unfold quantifiers (Ball, Bex, Ex1)

modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;

formal markup of @{syntax_const} and @{const_syntax}; authentic syntax for extra robustness;

modernized translations; formal markup of @{syntax_const} and @{const_syntax};

numeral syntax: clarify parse trees vs. actual terms; modernized translations; formal markup of @{syntax_const} and @{const_syntax};

added ML antiquotation @{syntax_const};

treat inner token markers as syntax consts;

modernized syntax/translations;

modernized syntax/translations; tuned headers;

modernized translations;

merged

use full paths when importing theories

merged

inductive vs inductive_set explanation

modernized translations;

modernized translations;

renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;

merged

Fixed bug in code for guessing the name of the variable representing the freshness context.

dropped last occurence of the linlinordered accident

dropped Id

minor metis proof tuning

merged

NEWS

moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy

revert uninspired Structure_Syntax experiment

moved lemma field_le_epsilon from Real.thy to Fields.thy

merged

unset KODKODI explicitly -- apparently isatest patches settings cumulatively;