src/HOL/Number_Theory/Residues.thy
changeset 35416 d8d7d1b785af
parent 32479 521cc9bf2958
child 36350 bc7982c54e37
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -22,8 +22,7 @@
     1.4  
     1.5  *)
     1.6  
     1.7 -constdefs 
     1.8 -  residue_ring :: "int => int ring"
     1.9 +definition residue_ring :: "int => int ring" where
    1.10    "residue_ring m == (| 
    1.11      carrier =       {0..m - 1}, 
    1.12      mult =          (%x y. (x * y) mod m),
    1.13 @@ -287,8 +286,7 @@
    1.14  
    1.15  (* the definition of the phi function *)
    1.16  
    1.17 -constdefs
    1.18 -  phi :: "int => nat"
    1.19 +definition phi :: "int => nat" where
    1.20    "phi m == card({ x. 0 < x & x < m & gcd x m = 1})" 
    1.21  
    1.22  lemma phi_zero [simp]: "phi 0 = 0"