1.1 --- a/src/Doc/Tutorial/Protocol/Public.thy	Thu Feb 28 14:22:14 2013 +0100
     1.2 +++ b/src/Doc/Tutorial/Protocol/Public.thy	Thu Feb 28 14:24:21 2013 +0100
     1.3 @@ -47,8 +47,8 @@
     1.4  any public key.
     1.5  *}
     1.6  
     1.7 -axioms
     1.8 -  inj_pubK:        "inj pubK"
     1.9 +axiomatization where
    1.10 +  inj_pubK:        "inj pubK" and
    1.11    priK_neq_pubK:   "priK A \<noteq> pubK B"
    1.12  (*<*)
    1.13  lemmas [iff] = inj_pubK [THEN inj_eq]