old domain package also defines map functions

separate map-related code into new function define_map_functions

removed Local_Theory.theory_result by using local Typedef.add_typedef

tuned comment;

observe standard header format;

expose formal text;

localized @{class} and @{type};

move functions into holcf_library.ML

simplify definition of when combinators

declare case_names for various induction rules

add case name 'adm' for infinite induction rules

renamed some lemmas generated by the domain package

use Simplifier.context to avoid 'no proof context in simpset' errors from fixrec_simp after theory merge

fixpat command prints legacy_feature warning

merged

pass binding as argument to add_domain_constructors; proper binding for case combinator

pass domain binding as argument to Domain_Theorems.theorems; proper qualified bindings for theorem names

pass take_info as argument to Domain_Theorems.theorems

replace some string arguments with bindings

more consistent use of qualified bindings

avoid unnecessary primed variable names

remove redundant lemmas

fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy

fixrec now generates qualified theorem names

no_document for Infinite_Set in HOLCF

removed unused Args.maxidx_values and Element.generalize_facts;

Local_Theory.define handles hidden polymorphism;

local theory specifications handle hidden polymorphism implicitly;

minor tuning and simplification;

removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0;

removed old CVS Ids; tuned headers;

reverted fe9b43a08187 -- "warning" is a perfectly normal way of tactics to emit spurious messages (although "arith" could be less chatty), while "priority" is a special Proof General protocol message;

merged

merged

adopting predicate compiler to changes in Spec_Rules; removed dependency to Nitpick_Intros

adding Spec_Rules to definitional package inductive and inductive_set

refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function

merged

Reorganized Hoare logic theories; added Hoare_Den

merged

reset smt_certificates

added lemmas

merged

Added Hoare_Op.thy

Equality of integral and infinite sum.

make tests less demanding, to prevent sporadic failures

more antiquotations;

command 'typedef' now works within a local theory context;

removed obsolete HOL 'typedecl'; local theory version of HOL 'typedef';

adapted to localized typedef: handle single global interpretation only;

global typedef;

localized typedef; Typedef.get_info can yield multiple typedef interpretations, even in a global context; misc tuning and modernization;

added typedecl_wrt, which affects default sorts of type args; misc tuning and simplification;

Local_Defs.contract convenience;

added Local_Theory.alias operations (independent of target);

merged

merged

converted proofs to Isar

merged

merged

tuned prefix of ac rules

deleted default simp rule card.insert

updated generated certificate

replaced card_def by card_eq_setsum

NEWS

Big_Operators now in Main rather than Plain

tuned prefixes of ac interpretations

Big_Operators now in Main rather than Plain src/HOL/Wellfounded.thy

fixed typo

tuned monoid locales and prefix of sublocale interpretations

moved cardinality to Finite_Set as far as appropriate; added locales for fold_image

fixed typo

added locales for monoids

split off theory Big_Operators from theory Finite_Set

moved some Nitpick code around

more basic Local_Defs.export_cterm;

tuned signature;

tuned;

actually apply morphism to binding;

absolute lib_path relative to ML_HOME -- for improved robustness; explicit warning if shared library failed to load;

added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets

added term postprocessor to Nitpick, to provide custom syntax for typedefs

made "Manual_Nits" tests more robust

merged

made smlnj happy

replace Nat_Int_Bij with Nat_Bijection in ROOT.ML

remove obsolete theory Nat_Int_Bij

switch from Nat_Int_Bij to Nat_Bijection

convert HOL-Probability to use Nat_Bijection library

convert SET_Protocol to use Nat_Bijection library

convert TLS to use Nat_Bijection library

adapt HOLCF to use Nat_Bijection library

new theory Library/Nat_Bijection.thy

improve precision of "card" in Nitpick

merged

merged

show nice error message in Nitpick when "java" is not available

fixed soundness bug in Nitpick

merged

Use same order of neq-elimination as in proof search.

Moved theorems in Lebesgue to the right places

constdefs is legacy

recdef is legacy

fixed typo

avoid confusion

tuned whitespace

merged

tuned

clarified transfer code proper; more natural declaration of return rules

misc tuning

Typedecl.typedecl_global;

localized typedecl;

aliases for class/type/const; tuned;

added Name_Space.alias -- additional accesses for an existing entry;

merged

merged

data administration using canonical functorial operations

tuned data structures; using AList.map_default

consistent field names; tuned interface

weakend class ring_div; tuned