--- a/src/HOL/Old_Number_Theory/IntPrimes.thy Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy Sat Oct 17 14:43:18 2009 +0200
@@ -26,10 +26,10 @@
"measure ((\<lambda>(m, n, r', r, s', s, t', t). nat r)
:: int * int * int * int *int * int * int * int => nat)"
"xzgcda (m, n, r', r, s', s, t', t) =
- (if r \<le> 0 then (r', s', t')
- else xzgcda (m, n, r, r' mod r,
- s, s' - (r' div r) * s,
- t, t' - (r' div r) * t))"
+ (if r \<le> 0 then (r', s', t')
+ else xzgcda (m, n, r, r' mod r,
+ s, s' - (r' div r) * s,
+ t, t' - (r' div r) * t))"
definition
zprime :: "int \<Rightarrow> bool" where