src/HOL/Library/Old_Recdef.thy
changeset 82299 a0693649e9c6
parent 69913 ca515cf61651
--- a/src/HOL/Library/Old_Recdef.thy	Mon Mar 17 11:30:39 2025 +0100
+++ b/src/HOL/Library/Old_Recdef.thy	Mon Mar 17 16:29:48 2025 +0100
@@ -82,6 +82,6 @@
   wf_measures
   wf_pred_nat
   wf_same_fst
-  wf_empty
+  wf_on_bot
 
 end