# HG changeset patch
# User wenzelm
# Date 1729722021 -7200
# Node ID 8205db6977dd503106bd99a796e5fd32873cec2c
# Parent  b162ff88bdc5cc12355c9d38094668c6634308eb
more robust: avoid ambiguity of contract_abbrevs;

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)"