author | wenzelm |
Thu, 24 Oct 2024 00:20:21 +0200 | |
changeset 81248 | 8205db6977dd |
parent 81247 | b162ff88bdc5 |
child 81249 | 389f315f8c24 |
--- 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)"