1.1 --- a/src/HOLCF/Adm.thy	Thu Jan 03 17:02:56 2008 +0100
     1.2 +++ b/src/HOLCF/Adm.thy	Thu Jan 03 17:22:24 2008 +0100
     1.3 @@ -200,37 +200,4 @@
     1.4    adm_less adm_eq adm_not_less
     1.5    adm_compact_not_less adm_compact_neq adm_neq_compact adm_not_UU
     1.6  
     1.7 -(* legacy ML bindings *)
     1.8 -ML
     1.9 -{*
    1.10 -val adm_def = thm "adm_def";
    1.11 -val admI = thm "admI";
    1.12 -val triv_admI = thm "triv_admI";
    1.13 -val admD = thm "admD";
    1.14 -val adm_max_in_chain = thm "adm_max_in_chain";
    1.15 -val adm_chfin = thm "adm_chfin";
    1.16 -val admI2 = thm "admI2";
    1.17 -val adm_less = thm "adm_less";
    1.18 -val adm_conj = thm "adm_conj";
    1.19 -val adm_not_free = thm "adm_not_free";
    1.20 -val adm_not_less = thm "adm_not_less";
    1.21 -val adm_all = thm "adm_all";
    1.22 -val adm_all2 = thm "adm_all2";
    1.23 -val adm_ball = thm "adm_ball";
    1.24 -val adm_ball2 = thm "adm_ball2";
    1.25 -val adm_subst = thm "adm_subst";
    1.26 -val adm_not_UU = thm "adm_not_UU";
    1.27 -val adm_eq = thm "adm_eq";
    1.28 -val adm_disj_lemma1 = thm "adm_disj_lemma1";
    1.29 -val adm_disj_lemma2 = thm "adm_disj_lemma2";
    1.30 -val adm_disj_lemma3 = thm "adm_disj_lemma3";
    1.31 -val adm_disj_lemma4 = thm "adm_disj_lemma4";
    1.32 -val adm_disj_lemma5 = thm "adm_disj_lemma5";
    1.33 -val adm_disj = thm "adm_disj";
    1.34 -val adm_imp = thm "adm_imp";
    1.35 -val adm_iff = thm "adm_iff";
    1.36 -val adm_not_conj = thm "adm_not_conj";
    1.37 -val adm_lemmas = thms "adm_lemmas";
    1.38 -*}
    1.39 -
    1.40  end

     2.1 --- a/src/HOLCF/Domain.thy	Thu Jan 03 17:02:56 2008 +0100
     2.2 +++ b/src/HOLCF/Domain.thy	Thu Jan 03 17:22:24 2008 +0100
     2.3 @@ -194,27 +194,4 @@
     2.4  
     2.5  lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3
     2.6  
     2.7 -
     2.8 -subsection {* Setting up the package *}
     2.9 -
    2.10 -ML {*
    2.11 -val iso_intro       = thm "iso.intro";
    2.12 -val iso_abs_iso     = thm "iso.abs_iso";
    2.13 -val iso_rep_iso     = thm "iso.rep_iso";
    2.14 -val iso_abs_strict  = thm "iso.abs_strict";
    2.15 -val iso_rep_strict  = thm "iso.rep_strict";
    2.16 -val iso_abs_defin'  = thm "iso.abs_defin'";
    2.17 -val iso_rep_defin'  = thm "iso.rep_defin'";
    2.18 -val iso_abs_defined = thm "iso.abs_defined";
    2.19 -val iso_rep_defined = thm "iso.rep_defined";
    2.20 -val iso_compact_abs = thm "iso.compact_abs";
    2.21 -val iso_compact_rep = thm "iso.compact_rep";
    2.22 -val iso_iso_swap    = thm "iso.iso_swap";
    2.23 -
    2.24 -val exh_start = thm "exh_start";
    2.25 -val ex_defined_iffs = thms "ex_defined_iffs";
    2.26 -val exh_casedist0 = thm "exh_casedist0";
    2.27 -val exh_casedists = thms "exh_casedists";
    2.28 -*}
    2.29 -
    2.30  end