src/HOL/NumberTheory/EvenOdd.thy
changeset 16663 13e9c402308b
parent 16417 9bc16273c2d4
child 18369 694ea14ab4f2
     1.1 --- a/src/HOL/NumberTheory/EvenOdd.thy	Fri Jul 01 14:55:05 2005 +0200
     1.2 +++ b/src/HOL/NumberTheory/EvenOdd.thy	Fri Jul 01 17:41:10 2005 +0200
     1.3 @@ -219,7 +219,7 @@
     1.4  
     1.5  (* An odd prime is greater than 2 *)
     1.6  
     1.7 -lemma zprime_zOdd_eq_grt_2: "p \<in> zprime ==> (p \<in> zOdd) = (2 < p)";
     1.8 +lemma zprime_zOdd_eq_grt_2: "zprime p ==> (p \<in> zOdd) = (2 < p)";
     1.9    apply (auto simp add: zOdd_def zprime_def)
    1.10    apply (drule_tac x = 2 in allE)
    1.11    apply (insert odd_iff_not_even [of p])