adjusted to cs. 8dfd816713c6

NEWS

merged

tuned proofs

ascii syntax for multiset order

switched notations for pointwise and multiset order

NEWS

NEWS

merged

switched notations for pointwise and multiset order

moved remaning class operations from Algebras.thy to Groups.thy

hide fact range_def

dropped reference to type classes

NEWS

filter out authentic const syntax;

slightly more abstract syntax mark/unmark operations;

tuned;

NEWS: authentic syntax for *all* term constants;

concrete syntax for all constructors, to workaround authentic syntax problem with domain package;

adapted to authentic syntax;

adapted to authentic syntax; misc cleanup and modernization;

adapted to authentic syntax;

authentic syntax for *all* term constants;

binder notation for default print_mode -- to avoid strange output if "xsymbols" is not active;

tuned headers; tuned proofs;

simplified syntax -- to make it work for authentic syntax;

modernized notation -- to make it work for authentic syntax;

proper markup of const syntax;

more precise dependencies;

added lemma

moved reduced Induct/SList back from AFP.

adjusted to changes in cs b987b803616d

disabled some old (fragile) isatests;

tuned settings; activated kodkodi, i.e. HOL-Nitpick_Examples;

fixed document;

eliminated opaque signature matching -- tends to cause problems with toplevel pp for abstract types;

made SML/NJ happy;

tuned;

authentic term syntax; more precise treatment of naming vs. binding; misc tuning;

Thm.def_binding;

moved ancient Drule.get_def to OldGoals.get_def;

quote the constant and theorem name with @{text}

merged

merged

local Simplifier.context; tuned tactic setup;

renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;

tuned message;

Lin_Arith.pre_tac: inherit proper simplifier context, and get rid of posthoc renaming of bound variables;

merged

context theorem is optional

added dest_comb

a simple concept for datatype invariants

using Code.bare_thms_of_cert

simplified

added code_abstype keyword

Initial version of HOL quotient package.

merge

added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s

fix bug in Nitpick's monotonicity code w.r.t. binary integers

merged

merged

get rid of many duplicate simp rule warnings

get rid of warnings about duplicate simp rules in all HOLCF theories

HOLCF-FOCUS depends on ex/Stream.thy

fix looping call to simplifier

merged

Use top-down rewriting to contract abbreviations.

Added function rewrite_term_top for top-down rewriting.

merged

added lemma

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