equal
deleted
inserted
replaced
7 There are no negative numbers; we have |
7 There are no negative numbers; we have |
8 m #- n = 0 iff m<=n and m #- n = succ(k) iff m>n. |
8 m #- n = 0 iff m<=n and m #- n = succ(k) iff m>n. |
9 Also, rec(m, 0, %z w.z) is pred(m). |
9 Also, rec(m, 0, %z w.z) is pred(m). |
10 *) |
10 *) |
11 |
11 |
12 header{*Arithmetic Operators and Their Definitions*} |
12 section{*Arithmetic Operators and Their Definitions*} |
13 |
13 |
14 theory Arith imports Univ begin |
14 theory Arith imports Univ begin |
15 |
15 |
16 text{*Proofs about elementary arithmetic: addition, multiplication, etc.*} |
16 text{*Proofs about elementary arithmetic: addition, multiplication, etc.*} |
17 |
17 |