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

more work on Nitpick's finite sets

improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"

ProofContext.read_class/read_type_name_proper;

added ProofContext.tsig_of -- proforma version for local name space only, not logical content; added ProofContext.read_type_name_proper; localized ProofContext.read_class/read_arity/cert_arity; localized ProofContext.class_space/type_space etc.;

simplified Syntax.basic_syntax (again); separate Syntax.type_ast_trs depending on read_class/read_type;

tuned -- eliminated Sign.intern_sort;

renamed mk_const_def to legacy_const_def, because of slightly odd Sign.intern_term;

added "finitize" option to Nitpick + remove dependency on "Coinductive_List"

merged

remove unnecessary error handling code

construct fully typed goal in proof of induction rule

don't generate rule foo.finites for non-flat domains; use take_induct rule to prove induction rule

remove redundant function arguments

include take_info within take_induct_info type

pass take_info as an argument to comp_theorems

pass take_induct_info as an argument to comp_theorems

add type take_induct_info

generate take_induct lemmas

move proofs of reach and take lemmas to domain_take_proofs.ML

move lemmas from Domain.thy to Domain_Aux.thy

move take-proofs stuff into new theory Domain_Aux.thy

add type take_info

add function add_qualified_def

merged

proper ML interface; further polishing

code simplification and tuning

Added inducts field to inductive_result.

transfer: avoid camel case, more standard coding conventions, misc tuning

transfer: avoid camel case

merged

generate separate qualified theorem name for each type's reach and take_lemma