eliminated legacy 'axioms';
authorwenzelm
Thu Feb 28 14:24:21 2013 +0100 (2013-02-28)
changeset 51310d2aeb3dffb8f
parent 51309 473303ef6e34
child 51311 337cfc42c9c8
eliminated legacy 'axioms';
src/Doc/Tutorial/Protocol/Public.thy
     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]