equal
deleted
inserted
replaced
13 defs |
13 defs |
14 sumhr_def |
14 sumhr_def |
15 "sumhr p |
15 "sumhr p |
16 == Abs_hypreal(UN X:Rep_hypnat(fst p). |
16 == Abs_hypreal(UN X:Rep_hypnat(fst p). |
17 UN Y: Rep_hypnat(fst(snd p)). |
17 UN Y: Rep_hypnat(fst(snd p)). |
18 hyprel```{%n::nat. sumr (X n) (Y n) (snd(snd p))})" |
18 hyprel``{%n::nat. sumr (X n) (Y n) (snd(snd p))})" |
19 |
19 |
20 constdefs |
20 constdefs |
21 NSsums :: [nat=>real,real] => bool (infixr 80) |
21 NSsums :: [nat=>real,real] => bool (infixr 80) |
22 "f NSsums s == (%n. sumr 0 n f) ----NS> s" |
22 "f NSsums s == (%n. sumr 0 n f) ----NS> s" |
23 |
23 |