--- a/src/HOL/NumberTheory/Chinese.thy Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/NumberTheory/Chinese.thy Tue Aug 07 16:36:52 2001 +0200
@@ -56,9 +56,9 @@
mhf_def:
"mhf mf n i ==
- if i = 0 then funprod mf 1 (n - 1)
- else if i = n then funprod mf 0 (n - 1)
- else funprod mf 0 (i - 1) * funprod mf (i + 1) (n - 1 - i)"
+ if i = 0 then funprod mf 1' (n - 1')
+ else if i = n then funprod mf 0 (n - 1')
+ else funprod mf 0 (i - 1') * funprod mf (Suc i) (n - 1' - i)"
xilin_sol_def:
"xilin_sol i n kf bf mf ==