catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example

mind the "s"

merged

NEWS

added missing separator

more accurate when registering new types

added Dlist

tuned text

distributed theory Algebras to theories Groups and Lattices

merged

proper distinction of code datatypes and abstypes

merged

merged

merged

lemma distinct_insert

proper header and subsection headings

remove unneeded premise from rat_floor_lemma and floor_Fract

Replaced Integration by Multivariate-Analysis/Real_Integration

Support for one-dimensional integration in Multivariate-Analysis

Equivalence between DERIV and one-dimensional derivation in Multivariate-Analysis

merged

add mixfix field to type Domain_Library.cons

remove unnecessary local

update to use fixrec package

merge

enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit

filter out trivial definitions in Nitpick (e.g. "Topology.topo" from AFP)

dropped references to old axclass from documentation

Fixed bug that caused (r)trancl_tac to crash when the term denoting the relation contained variables bound by meta level quantifiers.

fixed a few bugs in Nitpick and removed unreferenced variables

update the keywords files

rename print_maps to print_quotmaps

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