merged

now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"

renamed "ATP_Linkup" theory to "Sledgehammer"

renamed Sledgehammer structures

move Sledgehammer files in a directory of their own

merged

dropped odd interpretation of comm_monoid_mult into comm_monoid_add

lemma swap_inj_on, swap_product

meaningful transfer certificate

dropped odd interpretation of comm_monoid_mult into comm_monoid_add; consider Min.insert_idem as default simp rule

updated certificate

dropped odd interpretation of comm_monoid_mult into comm_monoid_add

added locales folding_one_(idem); various streamlining and tuning

generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add

tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)

added one-entry cache around Kodkod invocation

merged

solve error in "Nitpick_Mono" + short path when no finite functions are inferred

minor additions to Nitpick docs

NEWS: Nat_Bijection library

document "nitpick_choice_spec" attribute

fix typo in "nitpick_choice_spec" attribute name (singular, not plural)

added support for "specification" and "ax_specification" constructs to Nitpick

rollback of local typedef until problem with type-variables can be sorted out; fixed header

adjusted to changes in Finite_Set

merged

merged

tuned inductions

tuned;

moved old Sign.intern_term to the place where it is still used;

preserve full const name more carefully, and avoid slightly odd Sign.intern_term;

replaced type_syntax/term_syntax by uniform syntax_declaration;

merged

corrected disastrous syntax declarations

added stmaryrd for isasymSqinter

use headers consistently

no_document for theory Countable

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