src/HOL/Hilbert_Choice.thy
changeset 31454 2c0959ab073f
parent 31380 f25536c0bb80
child 31723 f5cafe803b55
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Thu Jun 04 15:28:58 2009 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Jun 04 15:28:58 2009 +0200
     1.3 @@ -12,9 +12,7 @@
     1.4  
     1.5  subsection {* Hilbert's epsilon *}
     1.6  
     1.7 -axiomatization
     1.8 -  Eps :: "('a => bool) => 'a"
     1.9 -where
    1.10 +axiomatization Eps :: "('a => bool) => 'a" where
    1.11    someI: "P x ==> P (Eps P)"
    1.12  
    1.13  syntax (epsilon)
    1.14 @@ -586,74 +584,6 @@
    1.15  by blast
    1.16  
    1.17  
    1.18 -text{*Many of these bindings are used by the ATP linkup, and not just by
    1.19 -legacy proof scripts.*}
    1.20 -ML
    1.21 -{*
    1.22 -val inv_def = thm "inv_def";
    1.23 -val Inv_def = thm "Inv_def";
    1.24 -
    1.25 -val someI = thm "someI";
    1.26 -val someI_ex = thm "someI_ex";
    1.27 -val someI2 = thm "someI2";
    1.28 -val someI2_ex = thm "someI2_ex";
    1.29 -val some_equality = thm "some_equality";
    1.30 -val some1_equality = thm "some1_equality";
    1.31 -val some_eq_ex = thm "some_eq_ex";
    1.32 -val some_eq_trivial = thm "some_eq_trivial";
    1.33 -val some_sym_eq_trivial = thm "some_sym_eq_trivial";
    1.34 -val choice = thm "choice";
    1.35 -val bchoice = thm "bchoice";
    1.36 -val inv_id = thm "inv_id";
    1.37 -val inv_f_f = thm "inv_f_f";
    1.38 -val inv_f_eq = thm "inv_f_eq";
    1.39 -val inj_imp_inv_eq = thm "inj_imp_inv_eq";
    1.40 -val inj_transfer = thm "inj_transfer";
    1.41 -val inj_iff = thm "inj_iff";
    1.42 -val inj_imp_surj_inv = thm "inj_imp_surj_inv";
    1.43 -val f_inv_f = thm "f_inv_f";
    1.44 -val surj_f_inv_f = thm "surj_f_inv_f";
    1.45 -val inv_injective = thm "inv_injective";
    1.46 -val inj_on_inv = thm "inj_on_inv";
    1.47 -val surj_imp_inj_inv = thm "surj_imp_inj_inv";
    1.48 -val surj_iff = thm "surj_iff";
    1.49 -val surj_imp_inv_eq = thm "surj_imp_inv_eq";
    1.50 -val bij_imp_bij_inv = thm "bij_imp_bij_inv";
    1.51 -val inv_equality = thm "inv_equality";
    1.52 -val inv_inv_eq = thm "inv_inv_eq";
    1.53 -val o_inv_distrib = thm "o_inv_distrib";
    1.54 -val image_surj_f_inv_f = thm "image_surj_f_inv_f";
    1.55 -val image_inv_f_f = thm "image_inv_f_f";
    1.56 -val inv_image_comp = thm "inv_image_comp";
    1.57 -val bij_image_Collect_eq = thm "bij_image_Collect_eq";
    1.58 -val bij_vimage_eq_inv_image = thm "bij_vimage_eq_inv_image";
    1.59 -val Inv_f_f = thm "Inv_f_f";
    1.60 -val f_Inv_f = thm "f_Inv_f";
    1.61 -val Inv_injective = thm "Inv_injective";
    1.62 -val inj_on_Inv = thm "inj_on_Inv";
    1.63 -val split_paired_Eps = thm "split_paired_Eps";
    1.64 -val Eps_split = thm "Eps_split";
    1.65 -val Eps_split_eq = thm "Eps_split_eq";
    1.66 -val wf_iff_no_infinite_down_chain = thm "wf_iff_no_infinite_down_chain";
    1.67 -val Inv_mem = thm "Inv_mem";
    1.68 -val Inv_f_eq = thm "Inv_f_eq";
    1.69 -val Inv_comp = thm "Inv_comp";
    1.70 -val tfl_some = thm "tfl_some";
    1.71 -val make_neg_rule = thm "make_neg_rule";
    1.72 -val make_refined_neg_rule = thm "make_refined_neg_rule";
    1.73 -val make_pos_rule = thm "make_pos_rule";
    1.74 -val make_neg_rule' = thm "make_neg_rule'";
    1.75 -val make_pos_rule' = thm "make_pos_rule'";
    1.76 -val make_neg_goal = thm "make_neg_goal";
    1.77 -val make_pos_goal = thm "make_pos_goal";
    1.78 -val conj_forward = thm "conj_forward";
    1.79 -val disj_forward = thm "disj_forward";
    1.80 -val disj_forward2 = thm "disj_forward2";
    1.81 -val all_forward = thm "all_forward";
    1.82 -val ex_forward = thm "ex_forward";
    1.83 -*}
    1.84 -
    1.85 -
    1.86  subsection {* Meson package *}
    1.87  
    1.88  use "Tools/meson.ML"
    1.89 @@ -668,4 +598,5 @@
    1.90  
    1.91  use "Tools/specification_package.ML"
    1.92  
    1.93 +
    1.94  end