Removal of the obsolete newN function
authorpaulson
Tue Jul 01 17:35:09 1997 +0200 (1997-07-01)
changeset 3478770939fecbb3
parent 3477 3aced7fa7d8b
child 3479 2aacd6f10654
Removal of the obsolete newN function
src/HOL/Auth/Public.thy
     1.1 --- a/src/HOL/Auth/Public.thy	Tue Jul 01 17:34:42 1997 +0200
     1.2 +++ b/src/HOL/Auth/Public.thy	Tue Jul 01 17:35:09 1997 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4  syntax
     1.5    priK    :: agent => key
     1.6  
     1.7 -translations
     1.8 +translations  (*BEWARE! expressions like  (inj priK)  will NOT work!*)
     1.9    "priK x"  == "invKey(pubK x)"
    1.10  
    1.11  consts  (*Initial states of agents -- parameter of the construction*)
    1.12 @@ -57,16 +57,9 @@
    1.13      "used evs == parts (UN lost B. sees lost B evs)"
    1.14  
    1.15  
    1.16 -(*Agents generate "random" nonces, uniquely determined by their argument.*)
    1.17 -consts
    1.18 -  newN  :: nat => nat
    1.19 -
    1.20  rules
    1.21 -
    1.22    (*Public keys are disjoint, and never clash with private keys*)
    1.23    inj_pubK        "inj pubK"
    1.24    priK_neq_pubK   "priK A ~= pubK B"
    1.25  
    1.26 -  inj_newN        "inj newN"
    1.27 -
    1.28  end