ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML

ZF/ind_syntax/prove_term: deleted

ZF/constructor, indrule, intr_elim: now call prove_goalw_cterm and

Logic.unvarify

ZF/ind_syntax/prove_term: deleted

ZF/constructor, indrule, intr_elim: now call prove_goalw_cterm and

Logic.unvarify

HOLCF/Lift1.thy: updated for new sum_case by using "case" syntax

overheads for inductive definitions, originally for CADE-12

ZF/ex/ROOT: added .ML to use command use "ex/twos_compl"

Should be able to delete this after fixing the treatment of orphans.

Should be able to delete this after fixing the treatment of orphans.

ZF/ex/Ntree: two new examples, maptree and maptree2

ZF/func/fun_extend3: new

ZF/func/cons_fun_eq: simplified proof

ZF/func/cons_fun_eq: simplified proof

ZF/Univ/Sigma_subset_univ, Transset_Pair_subset_univ: deleted

ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where

they can be proved trivially using eq_cs

ZF/domrange/XXX_empty: renamed XXX_0

they can be proved trivially using eq_cs

ZF/domrange/XXX_empty: renamed XXX_0

ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML

ZF/Finite: added the finite function space, A-||>B

ZF/InfDatatype: added rules for the above

ZF/InfDatatype: added rules for the above