# HG changeset patch
# User huffman
# Date 1199377344 -3600
# Node ID 2b976fcee6e591f37cb15e897304ed3e1c8e84d8
# Parent  5df82bb5b982633e4e63c4db8c0fd46fefbedbdf
remove legacy ML bindings

diff -r 5df82bb5b982 -r 2b976fcee6e5 src/HOLCF/Adm.thy
--- a/src/HOLCF/Adm.thy	Thu Jan 03 17:02:56 2008 +0100
+++ b/src/HOLCF/Adm.thy	Thu Jan 03 17:22:24 2008 +0100
@@ -200,37 +200,4 @@
   adm_less adm_eq adm_not_less
   adm_compact_not_less adm_compact_neq adm_neq_compact adm_not_UU
 
-(* legacy ML bindings *)
-ML
-{*
-val adm_def = thm "adm_def";
-val admI = thm "admI";
-val triv_admI = thm "triv_admI";
-val admD = thm "admD";
-val adm_max_in_chain = thm "adm_max_in_chain";
-val adm_chfin = thm "adm_chfin";
-val admI2 = thm "admI2";
-val adm_less = thm "adm_less";
-val adm_conj = thm "adm_conj";
-val adm_not_free = thm "adm_not_free";
-val adm_not_less = thm "adm_not_less";
-val adm_all = thm "adm_all";
-val adm_all2 = thm "adm_all2";
-val adm_ball = thm "adm_ball";
-val adm_ball2 = thm "adm_ball2";
-val adm_subst = thm "adm_subst";
-val adm_not_UU = thm "adm_not_UU";
-val adm_eq = thm "adm_eq";
-val adm_disj_lemma1 = thm "adm_disj_lemma1";
-val adm_disj_lemma2 = thm "adm_disj_lemma2";
-val adm_disj_lemma3 = thm "adm_disj_lemma3";
-val adm_disj_lemma4 = thm "adm_disj_lemma4";
-val adm_disj_lemma5 = thm "adm_disj_lemma5";
-val adm_disj = thm "adm_disj";
-val adm_imp = thm "adm_imp";
-val adm_iff = thm "adm_iff";
-val adm_not_conj = thm "adm_not_conj";
-val adm_lemmas = thms "adm_lemmas";
-*}
-
 end
diff -r 5df82bb5b982 -r 2b976fcee6e5 src/HOLCF/Domain.thy
--- a/src/HOLCF/Domain.thy	Thu Jan 03 17:02:56 2008 +0100
+++ b/src/HOLCF/Domain.thy	Thu Jan 03 17:22:24 2008 +0100
@@ -194,27 +194,4 @@
 
 lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3
 
-
-subsection {* Setting up the package *}
-
-ML {*
-val iso_intro       = thm "iso.intro";
-val iso_abs_iso     = thm "iso.abs_iso";
-val iso_rep_iso     = thm "iso.rep_iso";
-val iso_abs_strict  = thm "iso.abs_strict";
-val iso_rep_strict  = thm "iso.rep_strict";
-val iso_abs_defin'  = thm "iso.abs_defin'";
-val iso_rep_defin'  = thm "iso.rep_defin'";
-val iso_abs_defined = thm "iso.abs_defined";
-val iso_rep_defined = thm "iso.rep_defined";
-val iso_compact_abs = thm "iso.compact_abs";
-val iso_compact_rep = thm "iso.compact_rep";
-val iso_iso_swap    = thm "iso.iso_swap";
-
-val exh_start = thm "exh_start";
-val ex_defined_iffs = thms "ex_defined_iffs";
-val exh_casedist0 = thm "exh_casedist0";
-val exh_casedists = thms "exh_casedists";
-*}
-
 end