diff -r b162ff88bdc5 -r 8205db6977dd src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Wed Oct 23 23:46:07 2024 +0200
+++ b/src/HOL/Auth/Public.thy	Thu Oct 24 00:20:21 2024 +0200
@@ -46,11 +46,11 @@
 text\<open>These abbreviations give backward compatibility.  They represent the
 simple situation where the signature and encryption keys are the same.\<close>
 
-abbreviation
+abbreviation (input)
   pubK :: "agent \<Rightarrow> key" where
   "pubK A == pubEK A"
 
-abbreviation
+abbreviation (input)
   priK :: "agent \<Rightarrow> key" where
   "priK A == invKey (pubEK A)"