src/HOL/NumberTheory/Chinese.thy
changeset 11468 02cd5d5bc497
parent 11049 7eef34adb852
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/NumberTheory/Chinese.thy	Mon Aug 06 16:43:40 2001 +0200
     1.2 +++ b/src/HOL/NumberTheory/Chinese.thy	Tue Aug 07 16:36:52 2001 +0200
     1.3 @@ -56,9 +56,9 @@
     1.4  
     1.5    mhf_def:
     1.6      "mhf mf n i ==
     1.7 -      if i = 0 then funprod mf 1 (n - 1)
     1.8 -      else if i = n then funprod mf 0 (n - 1)
     1.9 -      else funprod mf 0 (i - 1) * funprod mf (i + 1) (n - 1 - i)"
    1.10 +      if i = 0 then funprod mf 1' (n - 1')
    1.11 +      else if i = n then funprod mf 0 (n - 1')
    1.12 +      else funprod mf 0 (i - 1') * funprod mf (Suc i) (n - 1' - i)"
    1.13  
    1.14    xilin_sol_def:
    1.15      "xilin_sol i n kf bf mf ==