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;