# HG changeset patch
# User paulson
# Date 867771309 -7200
# Node ID 770939fecbb3db1205e214e189f38835186bd9b0
# Parent  3aced7fa7d8b4b5a4fb0fd869d979ecc052d71a0
Removal of the obsolete newN function

diff -r 3aced7fa7d8b -r 770939fecbb3 src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Tue Jul 01 17:34:42 1997 +0200
+++ b/src/HOL/Auth/Public.thy	Tue Jul 01 17:35:09 1997 +0200
@@ -16,7 +16,7 @@
 syntax
   priK    :: agent => key
 
-translations
+translations  (*BEWARE! expressions like  (inj priK)  will NOT work!*)
   "priK x"  == "invKey(pubK x)"
 
 consts  (*Initial states of agents -- parameter of the construction*)
@@ -57,16 +57,9 @@
     "used evs == parts (UN lost B. sees lost B evs)"
 
 
-(*Agents generate "random" nonces, uniquely determined by their argument.*)
-consts
-  newN  :: nat => nat
-
 rules
-
   (*Public keys are disjoint, and never clash with private keys*)
   inj_pubK        "inj pubK"
   priK_neq_pubK   "priK A ~= pubK B"
 
-  inj_newN        "inj newN"
-
 end