| changeset 61830 | 4f5ab843cf5b |
| parent 32631 | 2489e3c3562b |
| child 62145 | 5b946c81dfbf |
--- a/src/HOL/Auth/All_Symmetric.thy Thu Dec 10 21:31:24 2015 +0100 +++ b/src/HOL/Auth/All_Symmetric.thy Thu Dec 10 21:39:33 2015 +0100 @@ -2,7 +2,7 @@ imports Message begin -text {* All keys are symmetric *} +text \<open>All keys are symmetric\<close> defs all_symmetric_def: "all_symmetric \<equiv> True"