added generator_dseq compilation for a sound depth-limited compilation with small value generators

for now safely but unpractically assume no predicate is terminating

adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible

adding option smart_depth_limiting to predicate compiler

merged

introduce function strict :: 'a -> 'b -> 'b, which works like Haskell's seq; use strict instead of strictify in various definitions

add lemma lub_eq_bottom_iff

combine check_and_sort_domain with main function; rewrite much of the error-checking code

constructor arguments with selectors must have pointed types

simplify check_and_sort_domain; more meaningful variable names

replace fixrec 'permissive' mode with per-equation 'unchecked' option

rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML

simplify some proofs; remove some unused lists of lemmas

replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function

eliminate constant 'coerce'; use 'prj oo emb' instead

simplify fixrec pattern match function

simplify some proofs

tuned

added some facts about factorial and dvd, div and mod

removing something that probably slipped into the Quotient_List theory

Quotient package: partial equivalence introduction

reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)

remove dead code

remove old uses of 'simp_tac HOLCF_ss'

merged

remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check

reimplement proof automation for coinduct rules

add functions mk_imp, mk_all