removed dead code
authorhuffman
Sat Feb 27 18:45:06 2010 -0800 (2010-02-27)
changeset 354642ae3362ba8ee
parent 35463 b20501588930
child 35465 064bb6e9ace0
removed dead code
src/HOLCF/Tools/Domain/domain_theorems.ML
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Feb 27 18:31:52 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Feb 27 18:45:06 2010 -0800
     1.3 @@ -32,20 +32,11 @@
     1.4  val adm_all = @{thm adm_all};
     1.5  val adm_conj = @{thm adm_conj};
     1.6  val adm_subst = @{thm adm_subst};
     1.7 -val antisym_less_inverse = @{thm below_antisym_inverse};
     1.8 -val beta_cfun = @{thm beta_cfun};
     1.9 -val cfun_arg_cong = @{thm cfun_arg_cong};
    1.10  val ch2ch_fst = @{thm ch2ch_fst};
    1.11  val ch2ch_snd = @{thm ch2ch_snd};
    1.12  val ch2ch_Rep_CFunL = @{thm ch2ch_Rep_CFunL};
    1.13  val ch2ch_Rep_CFunR = @{thm ch2ch_Rep_CFunR};
    1.14  val chain_iterate = @{thm chain_iterate};
    1.15 -val compact_ONE = @{thm compact_ONE};
    1.16 -val compact_sinl = @{thm compact_sinl};
    1.17 -val compact_sinr = @{thm compact_sinr};
    1.18 -val compact_spair = @{thm compact_spair};
    1.19 -val compact_up = @{thm compact_up};
    1.20 -val contlub_cfun_arg = @{thm contlub_cfun_arg};
    1.21  val contlub_cfun_fun = @{thm contlub_cfun_fun};
    1.22  val contlub_fst = @{thm contlub_fst};
    1.23  val contlub_snd = @{thm contlub_snd};
    1.24 @@ -56,33 +47,10 @@
    1.25  val cont2cont_snd = @{thm cont2cont_snd};
    1.26  val cont2cont_Rep_CFun = @{thm cont2cont_Rep_CFun};
    1.27  val fix_def2 = @{thm fix_def2};
    1.28 -val injection_eq = @{thm injection_eq};
    1.29 -val injection_less = @{thm injection_below};
    1.30  val lub_equal = @{thm lub_equal};
    1.31 -val monofun_cfun_arg = @{thm monofun_cfun_arg};
    1.32  val retraction_strict = @{thm retraction_strict};
    1.33 -val spair_eq = @{thm spair_eq};
    1.34 -val spair_less = @{thm spair_below};
    1.35 -val sscase1 = @{thm sscase1};
    1.36 -val ssplit1 = @{thm ssplit1};
    1.37 -val strictify1 = @{thm strictify1};
    1.38  val wfix_ind = @{thm wfix_ind};
    1.39 -
    1.40 -val iso_intro       = @{thm iso.intro};
    1.41 -val iso_abs_iso     = @{thm iso.abs_iso};
    1.42 -val iso_rep_iso     = @{thm iso.rep_iso};
    1.43 -val iso_abs_strict  = @{thm iso.abs_strict};
    1.44 -val iso_rep_strict  = @{thm iso.rep_strict};
    1.45 -val iso_abs_defined = @{thm iso.abs_defined};
    1.46 -val iso_rep_defined = @{thm iso.rep_defined};
    1.47 -val iso_compact_abs = @{thm iso.compact_abs};
    1.48 -val iso_compact_rep = @{thm iso.compact_rep};
    1.49 -val iso_iso_swap    = @{thm iso.iso_swap};
    1.50 -
    1.51 -val exh_start = @{thm exh_start};
    1.52 -val ex_defined_iffs = @{thms ex_defined_iffs};
    1.53 -val exh_casedist0 = @{thm exh_casedist0};
    1.54 -val exh_casedists = @{thms exh_casedists};
    1.55 +val iso_intro = @{thm iso.intro};
    1.56  
    1.57  open Domain_Library;
    1.58  infixr 0 ===>;
    1.59 @@ -135,8 +103,6 @@
    1.60  
    1.61  val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp}
    1.62  
    1.63 -val dist_eqI = @{lemma "!!x::'a::po. ~ x << y ==> x ~= y" by (blast dest!: below_antisym_inverse)}
    1.64 -
    1.65  fun theorems
    1.66      (((dname, _), cons) : eq, eqs : eq list)
    1.67      (dom_eqn : typ * (binding * (bool * binding option * typ) list * mixfix) list)
    1.68 @@ -196,12 +162,8 @@
    1.69  
    1.70  val pg = pg' thy;
    1.71  
    1.72 -val dc_abs  = %%:(dname^"_abs");
    1.73 -val dc_rep  = %%:(dname^"_rep");
    1.74  val dc_copy = %%:(dname^"_copy");
    1.75 -val x_name = "x";
    1.76  
    1.77 -val iso_locale = iso_intro OF [ax_abs_iso, ax_rep_iso];
    1.78  val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
    1.79  val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
    1.80  val iso_rews = map Drule.export_without_context [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];