# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1643386528 0
# Node ID ccf203c9b2db764d5f2b6f32fe424ac0eb2ac3b6
# Parent  7483347efb4ca5b2eea6625aaea25031414036e6
Deletion of a duplicate proof

diff -r 7483347efb4c -r ccf203c9b2db src/HOL/Examples/Ackermann.thy
--- 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>