changeset 35705 | 0e5251adb9cc |
parent 33615 | 261abc2e3155 |
child 39757 | 21423597a80d |
--- a/src/HOL/SET_Protocol/ROOT.ML Wed Mar 10 15:57:01 2010 -0800 +++ b/src/HOL/SET_Protocol/ROOT.ML Wed Mar 10 15:58:53 2010 -0800 @@ -5,5 +5,5 @@ Root file for the SET protocol proofs. *) -no_document use_thys ["Nat_Int_Bij"]; +no_document use_thys ["Nat_Bijection"]; use_thys ["Cardholder_Registration", "Merchant_Registration", "Purchase"];