equal
deleted
inserted
replaced
20 quotient and remainder using ML and checking the answer using multiplication |
20 quotient and remainder using ML and checking the answer using multiplication |
21 by proof. Then uniqueness of the quotient and remainder yields theorems |
21 by proof. Then uniqueness of the quotient and remainder yields theorems |
22 quoting the previously computed values. (Or code an oracle...) |
22 quoting the previously computed values. (Or code an oracle...) |
23 *) |
23 *) |
24 |
24 |
25 Bin = Integ + Datatype + |
25 Bin = Int + Datatype + |
26 |
26 |
27 syntax |
27 syntax |
28 "_Int" :: xnum => int ("_") |
28 "_Int" :: xnum => int ("_") |
29 |
29 |
30 datatype |
30 datatype |