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

reorganize Bifinite.thy; simplify some proofs related to bifinite class instances

treat pervasive "Interrupt" constructor as illegal -- superseded by Exn.Interrupt for internal use and Exn.is_interrupt/Exn.interrupt in user-space;

Laze.force_result: more robust treatment of interrupts stemming from peer group cancellation;

more precise treatment of deleted nodes;

tuned error message;