Lines Matching defs:n1
183 val n1 = length L1
185 val (turn, L1, L2, n1, n2) =
186 if n1 <= n2 then (false, L1, L2, n1, n2) else
187 (true, L2, L1, n2, n1)
192 val thm1 = if n1 = n2 then thm0 else
194 val (L21, L22) = Lib.split_after (n2 - n1) L2
253 val n1 = length L1
255 val (turn, L1, L2, n1, n2) =
256 if n1 <= n2 then (false, L1, L2, n1, n2) else
257 (true, L2, L1, n2, n1)
262 val thm1 = if n1 = n2 then thm0 else
264 val (L21, L22) = Lib.split_after n1 L2