more robust: avoid ambiguity of contract_abbrevs;
authorwenzelm
Thu, 24 Oct 2024 00:20:21 +0200
changeset 81248 8205db6977dd
parent 81247 b162ff88bdc5
child 81249 389f315f8c24
more robust: avoid ambiguity of contract_abbrevs;
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)"