src/HOL/Hilbert_Choice.thy
changeset 11506 244a02a2968b
parent 11454 7514e5e21cb8
child 12023 d982f98e0f0d
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Tue Aug 28 14:25:26 2001 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Wed Aug 29 21:17:24 2001 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  
     1.5  
     1.6  syntax (input)
     1.7 -  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\\<epsilon>_./ _)" [0, 10] 10)
     1.8 +  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\<epsilon>_./ _)" [0, 10] 10)
     1.9  
    1.10  syntax (HOL)
    1.11    "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3@ _./ _)" [0, 10] 10)
    1.12 @@ -30,7 +30,7 @@
    1.13  
    1.14  
    1.15  (*used in TFL*)
    1.16 -lemma tfl_some: "\\<forall>P x. P x --> P (Eps P)"
    1.17 +lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
    1.18    by (blast intro: someI)
    1.19  
    1.20  
    1.21 @@ -59,7 +59,7 @@
    1.22  
    1.23  lemma LeastMI2:
    1.24    "[| P x; !!y. P y ==> m x <= m y;
    1.25 -           !!x. [| P x; \\<forall>y. P y --> m x \\<le> m y |] ==> Q x |]
    1.26 +           !!x. [| P x; \<forall>y. P y --> m x \<le> m y |] ==> Q x |]
    1.27     ==> Q (LeastM m P)";
    1.28  apply (unfold LeastM_def)
    1.29  apply (rule someI2_ex)
    1.30 @@ -128,7 +128,7 @@
    1.31  lemma GreatestMI2:
    1.32       "[| P x;
    1.33  	 !!y. P y ==> m y <= m x;
    1.34 -         !!x. [| P x; \\<forall>y. P y --> m y \\<le> m x |] ==> Q x |]
    1.35 +         !!x. [| P x; \<forall>y. P y --> m y \<le> m x |] ==> Q x |]
    1.36        ==> Q (GreatestM m P)";
    1.37  apply (unfold GreatestM_def)
    1.38  apply (rule someI2_ex)
    1.39 @@ -203,20 +203,6 @@
    1.40  done
    1.41  
    1.42  
    1.43 -ML {*
    1.44 -val LeastMI2 = thm "LeastMI2";
    1.45 -val LeastM_equality = thm "LeastM_equality";
    1.46 -val GreatestM_def = thm "GreatestM_def";
    1.47 -val GreatestMI2 = thm "GreatestMI2";
    1.48 -val GreatestM_equality = thm "GreatestM_equality";
    1.49 -val Greatest_def = thm "Greatest_def";
    1.50 -val Greatest_equality = thm "Greatest_equality";
    1.51 -val GreatestM_natI = thm "GreatestM_natI";
    1.52 -val GreatestM_nat_le = thm "GreatestM_nat_le";
    1.53 -val GreatestI = thm "GreatestI";
    1.54 -val Greatest_le = thm "Greatest_le";
    1.55 -*}
    1.56 -
    1.57  use "meson_lemmas.ML"
    1.58  use "Tools/meson.ML"
    1.59  setup meson_setup