--- a/src/HOL/Examples/Ackermann.thy Thu Jan 27 12:25:24 2022 +0000
+++ b/src/HOL/Examples/Ackermann.thy Fri Jan 28 16:15:28 2022 +0000
@@ -61,9 +61,6 @@
"ackloop_dom (ack m n # l) \<Longrightarrow> ackloop_dom (n # m # l)"
by (induction m n arbitrary: l rule: ack.induct) auto
-lemma "ackloop_dom (ack m n # l) \<Longrightarrow> ackloop_dom (n # m # l)"
- by (induction m n arbitrary: l rule: ack.induct) auto
-
text\<open>This function codifies what @{term ackloop} is designed to do.
Proving the two functions equivalent also shows that @{term ackloop} can be used
to compute Ackermann's function.\<close>