merged

adding ROOT.ML to HOL-Mutabelle session; uncommenting HOL.induct constants in Mutabelle session

adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening

separated narrowing timeouts for intermediate and final steps

merged

merged

dropped axclass; dropped Id; session theory Hoare.thy

dropped session W0; c.f. MiniML in AFP

dropped axclass, going back to purely syntactic type classes

dropped axclass; dropped Id

dropped axclass; dropped Id; session theory Hoare.thy

dropped axclass

export prs_rules and rsp_rules attributes

merge

improved precision of small sets in Nitpick

improved Nitpick's support for quotient types

Forgot to check NSA in changeset e4a431b6d9b7 ; Removed import of Integration

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

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;

make Nitpick test a bit weaker; this should solve failure observed last night on "mac-poly"