# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1617362669 -3600
# Node ID c89922715bf5e6c36e20bab0304afc87bcdc888d
# Parent  c72fd8f1fcebaf86006caa552590b94dd8bdfbce
Cosmetic: no !! in the lemma statement

diff -r c72fd8f1fceb -r c89922715bf5 src/HOL/Examples/Ackermann.thy
--- a/src/HOL/Examples/Ackermann.thy	Thu Apr 01 07:35:03 2021 +0200
+++ b/src/HOL/Examples/Ackermann.thy	Fri Apr 02 12:24:29 2021 +0100
@@ -44,26 +44,16 @@
 
 text \<open>Termination is trivial if the length of the list is less then two.
 The following lemma is the key to proving termination for longer lists.\<close>
-lemma "\<And>n l. ackloop_dom (ack m n # l) \<Longrightarrow> ackloop_dom (n # m # l)"
-proof (induction m)
+lemma "ackloop_dom (ack m n # l) \<Longrightarrow> ackloop_dom (n # m # l)"
+proof (induction m arbitrary: n l)
   case 0
   then show ?case
     by auto
 next
   case (Suc m)
-  note IH = Suc
-  have "\<And>l. ackloop_dom (ack (Suc m) n # l) \<Longrightarrow> ackloop_dom (n # Suc m # l)"
-  proof (induction n)
-    case 0
-    then show ?case
-      by (simp add: IH)
-  next
-    case (Suc n)
-    then show ?case
-      by (auto simp: IH)
-  qed
-  then show ?case
-    using Suc.prems by blast
+  show ?case
+    using Suc.prems
+    by (induction n arbitrary: l) (simp_all add: Suc)
 qed
 
 text \<open>The proof above (which actually is unused) can be expressed concisely as follows.\<close>