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