changeset 61956 | 38b73f7940af |
parent 61830 | 4f5ab843cf5b |
child 67613 | ce654b0e6d69 |
--- a/src/HOL/Auth/Guard/Guard_Public.thy Mon Dec 28 21:47:32 2015 +0100 +++ b/src/HOL/Auth/Guard/Guard_Public.thy Mon Dec 28 23:13:33 2015 +0100 @@ -14,7 +14,7 @@ subsubsection\<open>signature\<close> definition sign :: "agent => msg => msg" where -"sign A X == {|Agent A, X, Crypt (priK A) (Hash X)|}" +"sign A X == \<lbrace>Agent A, X, Crypt (priK A) (Hash X)\<rbrace>" lemma sign_inj [iff]: "(sign A X = sign A' X') = (A=A' & X=X')" by (auto simp: sign_def)