--- a/src/HOL/Number_Theory/Residues.thy Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Number_Theory/Residues.thy Mon Mar 01 13:40:23 2010 +0100
@@ -22,8 +22,7 @@
*)
-constdefs
- residue_ring :: "int => int ring"
+definition residue_ring :: "int => int ring" where
"residue_ring m == (|
carrier = {0..m - 1},
mult = (%x y. (x * y) mod m),
@@ -287,8 +286,7 @@
(* the definition of the phi function *)
-constdefs
- phi :: "int => nat"
+definition phi :: "int => nat" where
"phi m == card({ x. 0 < x & x < m & gcd x m = 1})"
lemma phi_zero [simp]: "phi 0 = 0"