--- a/src/HOL/Divides.thy Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Divides.thy Tue Oct 16 23:12:45 2007 +0200
@@ -12,8 +12,8 @@
begin
class div = times +
- fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>div" 70)
- fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>mod" 70)
+ fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
+ fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
instance nat :: Divides.div
div_def: "m div n == wfrec (pred_nat^+)
@@ -22,12 +22,12 @@
(%f j. if j<n | n=0 then j else f (j-n)) m" ..
definition (in div)
- dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<^loc>dvd" 50)
+ dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50)
where
- [code func del]: "m \<^loc>dvd n \<longleftrightarrow> (\<exists>k. n = m \<^loc>* k)"
+ [code func del]: "m dvd n \<longleftrightarrow> (\<exists>k. n = m * k)"
class dvd_mod = div + zero + -- {* for code generation *}
- assumes dvd_def_mod [code func]: "x \<^loc>dvd y \<longleftrightarrow> y \<^loc>mod x = \<^loc>0"
+ assumes dvd_def_mod [code func]: "x dvd y \<longleftrightarrow> y mod x = 0"
definition
quorem :: "(nat*nat) * (nat*nat) => bool" where