# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1666018841 -3600
# Node ID e5162a8baa2458d3e70d0b994491746bfb19fba6
# Parent  f89f4aab1cc445aa39a7dcf09a1a08d3df7a0f60
tiny renaming

diff -r f89f4aab1cc4 -r e5162a8baa24 src/HOL/Examples/Ackermann.thy
--- a/src/HOL/Examples/Ackermann.thy	Mon Oct 17 14:53:09 2022 +0100
+++ b/src/HOL/Examples/Ackermann.thy	Mon Oct 17 16:00:41 2022 +0100
@@ -102,7 +102,7 @@
 | "ack_mset [x] = {#}"
 | "ack_mset (z#y#l) = mset ((y,z) # map (\<lambda>x. (Suc x, 0)) l)"
 
-lemma base: "ack_mset (Suc n # l) < add_mset (0,n) {# (Suc x, 0). x \<in># mset l #}"
+lemma case1: "ack_mset (Suc n # l) < add_mset (0,n) {# (Suc x, 0). x \<in># mset l #}"
 proof (cases l)
   case (Cons m list)
   have "{#(m, Suc n)#} < {#(Suc m, 0)#}"
@@ -128,7 +128,7 @@
 text \<open>In each recursive call, the function @{term ack_mset} decreases according to the multiset
 ordering.\<close>
 termination
-  by (relation "inv_image {(x,y). x<y} ack_mset") (auto simp: wf base)
+  by (relation "inv_image {(x,y). x<y} ack_mset") (auto simp: wf case1)
 
 text \<open>Another shortcut compared with before: equivalence follows directly from this lemma.\<close>
 lemma Ackloop_ack: "Ackloop (n # m # l) = Ackloop (ack m n # l)"