src/HOL/Auth/ROOT.ML
changeset 14716 1846cc85ada1
parent 14307 1cbc24648cf7
child 17394 a8c9ed3f9818
     1.1 --- a/src/HOL/Auth/ROOT.ML	Fri May 07 14:10:14 2004 +0200
     1.2 +++ b/src/HOL/Auth/ROOT.ML	Fri May 07 20:32:40 2004 +0200
     1.3 @@ -6,6 +6,8 @@
     1.4  Root file for protocol proofs.
     1.5  *)
     1.6  
     1.7 +no_document use_thy "NatPair";
     1.8 +
     1.9  set timing;
    1.10  
    1.11  (*Shared-key protocols*)