# HG changeset patch
# User huffman
# Date 1234623208 28800
# Node ID 9433df0998485b7a553c28afcf331baa6bd02c0b
# Parent  b82ab2aebbbf3a041b7079552242e75bc51fec36
fix document generation

diff -r b82ab2aebbbf -r 9433df099848 src/HOL/SET-Protocol/ROOT.ML
--- a/src/HOL/SET-Protocol/ROOT.ML	Sat Feb 14 01:24:01 2009 -0800
+++ b/src/HOL/SET-Protocol/ROOT.ML	Sat Feb 14 06:53:28 2009 -0800
@@ -6,4 +6,5 @@
 Root file for the SET protocol proofs.
 *)
 
+no_document use_thy "Nat_Int_Bij";
 use_thys ["Cardholder_Registration", "Merchant_Registration", "Purchase"];