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