improve support for mutual recursion: now generates correct copy constant and induction theorem for mutually-recursive types; initial support for indirect recursion

reimplement copy_def to use data constructor constants

cleaned up; renamed library function mk_cRep_CFun to list_ccomb; replaced rep_TFree with dest_TFree; added functions spair, mk_stuple

generate lambda pattern syntax for new data constructors

changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF

add constant one_when; LAM pattern for ONE

add translation for wildcard pattern

change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up

make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1

cleaned up; ch2ch_Rep_CFun is a simp rule

changed iterate to a continuous type

reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less

removed ex/loeckx.ML

removed proof about Ifix, which no longer exists

cleaned up; chain_const and thelub_const are simp rules

cleaned up; removed adm_tricks in favor of compactness theorems

fix spelling

Moved atom stuff to new file nominal_atoms.ML

- completed the list of thms for supp_atm - cleaned up the way how thms are collected under single names

Added code for proving that new datatype has finite support.

removed unused modify_typargs, map_typargs, fold_typargs;

added Isar.state/exn;

Isar.loop;

moved consts declarations to consts.ML;

Consts.dest;

Polymorphic constants.

added consts.ML;

fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;

dist_eqI: the_context();

Sign.const_monomorphic;