let the theory formally depend on the Boogie output

look for certificates relative to the theory

dropped numerals from monomorphization blacklist (only particular numerals are builtin, all other numerals should be treated uninterpreted), this blacklist should contain only truely polymorphic builtin constants supported by SMT

merged

update Theory.requires with new theory name

tuned signatures;

never open Unsynchronized;

merged

section headings

reorder chapters for generated document

merge Representable.thy into Domain.thy

move stuff from Domain.thy to Domain_Aux.thy

move map functions to new theory file Map_Functions; add theory file Plain_HOLCF

allow unpointed lazy arguments for definitional domain package

add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas

merged

removed unused lemma chain_mono2

rename class 'bifinite' to 'domain'

instance sum :: (predomain, predomain) predomain

configure sum type for fixrec

add class liftdomain, for bifinite domains where DEFL('a u) = u_defl('a)

instance prod :: (predomain, predomain) predomain

adapt isodefl proof script to unpointed types

add 'predomain' class: unpointed version of bifinite

add bifiniteness check for domain_isomorphism command

implement map_of_typ using Pattern.rewrite_term

avoid using stale theory

implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data

add function the_sort

refactor tmp_thy code