made smlnj happy

adding depth to predicate compile quickcheck for mutabelle tests; removing obsolete references in predicate compile quickcheck

adding HOL-Mutabelle to tests

merged

more explicit naming scheme

merged

adapt to changed variable name in casedist theorem

remove dependency on domain_syntax.ML

update HOLCF makefile

simplify add_axioms function; remove obsolete domain_syntax.ML

proof scripts use variable name y for casedist

fixrec and repdef modules import holcf_library

use y as variable name in casedist, like datatype package

proper names for types cfun, sprod, ssum

variable name changed

fix proof script for take_apps so it works with indirect recursion

remove dead code

remove unused mixfix component from type cons

cleaned up, added type annotations

remove unused selector field from type arg

add_syntax no longer needs a definitional mode

add_axioms no longer needs a definitional mode

get rid of primes on thy variables

move definition of finiteness predicate into domain_take_proofs.ML

move take-related definitions and proofs to new module; simplify map_of_typ functions

remove map_tab argument to calc_axioms

remove dead code

merged

Slightly generalised a theorem

merged