add class bifinite_cpo for possibly-unpointed bifinite domains

cleaned up instance proofs

new-style instantiation proof for unit :: po

class bifinite supersedes class dcpo; remove unnecessary dcpo stuff

simplified chfin instance proof

new theory of powerdomains

new theory of bifinite domains

new-style class instantiation

added lemmas lub_distribs

*** empty log message ***

*** empty log message ***

compact_chfin is now declared simp

use new-style class for po

add lemma contI2

converted adm_all and adm_ball to rule_format; cleaned up

Equations for constants without arguments are now declared using "val" instead of "fun".

new theory defining set as a pcpo

Test data generation and conversion to terms are now more closely intertwined, to allow displaying of functions in test data.

New example involving functions.

Now uses more carefully designed simpsets to prevent proofs from failing for some strange datatypes with nested recursion.

Test data generation and conversion to terms is now more closely intertwined, to allow displaying of functions in test data.

Eliminated DatatypeAux.dest_TFree to avoid clashes with Term.dest_TFree.

Added nil_const and cons_const.

Added test data generator for function type (from Pure/codegen.ML).

New interface for test data generators.

declare ch2ch_LAM [simp]

added overloading target

new compactness lemmas; removed duplicated flat_less_iff

Compactness subsection with new lemmas

Compactness subsection with some new lemmas