dropped legacy ML bindings; tuned
authorhaftmann
Thu Jun 04 15:28:58 2009 +0200 (2009-06-04)
changeset 314542c0959ab073f
parent 31453 78280bd2860a
child 31455 2754a0dadccc
dropped legacy ML bindings; tuned
src/HOL/Hilbert_Choice.thy
src/HOL/Tools/meson.ML
src/HOL/Tools/res_axioms.ML
     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
     2.1 --- a/src/HOL/Tools/meson.ML	Thu Jun 04 15:28:58 2009 +0200
     2.2 +++ b/src/HOL/Tools/meson.ML	Thu Jun 04 15:28:58 2009 +0200
     2.3 @@ -46,6 +46,19 @@
     2.4  val max_clauses_default = 60;
     2.5  val (max_clauses, setup) = Attrib.config_int "max_clauses" max_clauses_default;
     2.6  
     2.7 +val disj_forward = @{thm disj_forward};
     2.8 +val disj_forward2 = @{thm disj_forward2};
     2.9 +val make_pos_rule = @{thm make_pos_rule};
    2.10 +val make_pos_rule' = @{thm make_pos_rule'};
    2.11 +val make_pos_goal = @{thm make_pos_goal};
    2.12 +val make_neg_rule = @{thm make_neg_rule};
    2.13 +val make_neg_rule' = @{thm make_neg_rule'};
    2.14 +val make_neg_goal = @{thm make_neg_goal};
    2.15 +val conj_forward = @{thm conj_forward};
    2.16 +val all_forward = @{thm all_forward};
    2.17 +val ex_forward = @{thm ex_forward};
    2.18 +val choice = @{thm choice};
    2.19 +
    2.20  val not_conjD = thm "meson_not_conjD";
    2.21  val not_disjD = thm "meson_not_disjD";
    2.22  val not_notD = thm "meson_not_notD";
     3.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Jun 04 15:28:58 2009 +0200
     3.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Jun 04 15:28:58 2009 +0200
     3.3 @@ -258,7 +258,7 @@
     3.4        val cex = Thm.cterm_of thy (HOLogic.exists_const T)
     3.5        val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
     3.6        and conc =  c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
     3.7 -      fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS someI_ex) 1
     3.8 +      fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS @{thm someI_ex}) 1
     3.9    in  Goal.prove_internal [ex_tm] conc tacf
    3.10         |> forall_intr_list frees
    3.11         |> Thm.forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)