equal
deleted
inserted
replaced
92 \<close> |
92 \<close> |
93 |
93 |
94 ML \<open>factorial 42\<close> |
94 ML \<open>factorial 42\<close> |
95 ML \<open>factorial 10000 div factorial 9999\<close> |
95 ML \<open>factorial 10000 div factorial 9999\<close> |
96 |
96 |
97 text \<open>See @{url "http://mathworld.wolfram.com/AckermannFunction.html"}\<close> |
97 text \<open>See \<^url>\<open>http://mathworld.wolfram.com/AckermannFunction.html\<close>.\<close> |
98 |
98 |
99 ML \<open> |
99 ML \<open> |
100 fun ackermann 0 n = n + 1 |
100 fun ackermann 0 n = n + 1 |
101 | ackermann m 0 = ackermann (m - 1) 1 |
101 | ackermann m 0 = ackermann (m - 1) 1 |
102 | ackermann m n = ackermann (m - 1) (ackermann m (n - 1)) |
102 | ackermann m n = ackermann (m - 1) (ackermann m (n - 1)) |