avoid ML bindings;
authorwenzelm
Wed Aug 29 21:17:24 2001 +0200 (2001-08-29)
changeset 11506244a02a2968b
parent 11505 a410fa8acfca
child 11507 4b32a46ffd29
avoid ML bindings;
src/HOL/GroupTheory/Exponent.ML
src/HOL/Hilbert_Choice.thy
     1.1 --- a/src/HOL/GroupTheory/Exponent.ML	Tue Aug 28 14:25:26 2001 +0200
     1.2 +++ b/src/HOL/GroupTheory/Exponent.ML	Wed Aug 29 21:17:24 2001 +0200
     1.3 @@ -229,14 +229,14 @@
     1.4  
     1.5  Goal "[|p^k dvd n;  p\\<in>prime;  0<n|] ==> k <= exponent p n";
     1.6  by (asm_full_simp_tac (simpset() addsimps [exponent_def]) 1); 
     1.7 -by (etac Greatest_le 1);
     1.8 +by (etac (thm "Greatest_le") 1);
     1.9  by (blast_tac (claset() addDs [prime_imp_one_less, power_dvd_bound]) 1);  
    1.10  qed_spec_mp "exponent_ge";
    1.11  
    1.12  Goal "0<s ==> (p ^ exponent p s) dvd s";
    1.13  by (simp_tac (simpset() addsimps [exponent_def]) 1); 
    1.14  by (Clarify_tac 1); 
    1.15 -by (res_inst_tac [("k","0")] GreatestI 1);
    1.16 +by (res_inst_tac [("k","0")] (thm "GreatestI") 1);
    1.17  by (blast_tac (claset() addDs [prime_imp_one_less, power_dvd_bound]) 2);  
    1.18  by (Asm_full_simp_tac 1); 
    1.19  qed "power_exponent_dvd";
    1.20 @@ -251,7 +251,7 @@
    1.21  
    1.22  Goal "p\\<in>prime ==> exponent p (p^a) = a";
    1.23  by (asm_simp_tac (simpset() addsimps [exponent_def]) 1);
    1.24 -by (rtac Greatest_equality 1); 
    1.25 +by (rtac (thm "Greatest_equality") 1); 
    1.26  by (Asm_full_simp_tac 1);
    1.27  by (asm_simp_tac (simpset() addsimps [prime_imp_one_less, power_dvd_imp_le]) 1); 
    1.28  qed "exponent_power_eq";
     2.1 --- a/src/HOL/Hilbert_Choice.thy	Tue Aug 28 14:25:26 2001 +0200
     2.2 +++ b/src/HOL/Hilbert_Choice.thy	Wed Aug 29 21:17:24 2001 +0200
     2.3 @@ -14,7 +14,7 @@
     2.4  
     2.5  
     2.6  syntax (input)
     2.7 -  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\\<epsilon>_./ _)" [0, 10] 10)
     2.8 +  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\<epsilon>_./ _)" [0, 10] 10)
     2.9  
    2.10  syntax (HOL)
    2.11    "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3@ _./ _)" [0, 10] 10)
    2.12 @@ -30,7 +30,7 @@
    2.13  
    2.14  
    2.15  (*used in TFL*)
    2.16 -lemma tfl_some: "\\<forall>P x. P x --> P (Eps P)"
    2.17 +lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
    2.18    by (blast intro: someI)
    2.19  
    2.20  
    2.21 @@ -59,7 +59,7 @@
    2.22  
    2.23  lemma LeastMI2:
    2.24    "[| P x; !!y. P y ==> m x <= m y;
    2.25 -           !!x. [| P x; \\<forall>y. P y --> m x \\<le> m y |] ==> Q x |]
    2.26 +           !!x. [| P x; \<forall>y. P y --> m x \<le> m y |] ==> Q x |]
    2.27     ==> Q (LeastM m P)";
    2.28  apply (unfold LeastM_def)
    2.29  apply (rule someI2_ex)
    2.30 @@ -128,7 +128,7 @@
    2.31  lemma GreatestMI2:
    2.32       "[| P x;
    2.33  	 !!y. P y ==> m y <= m x;
    2.34 -         !!x. [| P x; \\<forall>y. P y --> m y \\<le> m x |] ==> Q x |]
    2.35 +         !!x. [| P x; \<forall>y. P y --> m y \<le> m x |] ==> Q x |]
    2.36        ==> Q (GreatestM m P)";
    2.37  apply (unfold GreatestM_def)
    2.38  apply (rule someI2_ex)
    2.39 @@ -203,20 +203,6 @@
    2.40  done
    2.41  
    2.42  
    2.43 -ML {*
    2.44 -val LeastMI2 = thm "LeastMI2";
    2.45 -val LeastM_equality = thm "LeastM_equality";
    2.46 -val GreatestM_def = thm "GreatestM_def";
    2.47 -val GreatestMI2 = thm "GreatestMI2";
    2.48 -val GreatestM_equality = thm "GreatestM_equality";
    2.49 -val Greatest_def = thm "Greatest_def";
    2.50 -val Greatest_equality = thm "Greatest_equality";
    2.51 -val GreatestM_natI = thm "GreatestM_natI";
    2.52 -val GreatestM_nat_le = thm "GreatestM_nat_le";
    2.53 -val GreatestI = thm "GreatestI";
    2.54 -val Greatest_le = thm "Greatest_le";
    2.55 -*}
    2.56 -
    2.57  use "meson_lemmas.ML"
    2.58  use "Tools/meson.ML"
    2.59  setup meson_setup