changeset 33615 | 261abc2e3155 |
parent 33028 | 9aa8bfb1649d |
child 35705 | 0e5251adb9cc |
--- a/src/HOL/SET_Protocol/ROOT.ML Wed Nov 11 09:02:37 2009 +0100 +++ b/src/HOL/SET_Protocol/ROOT.ML Wed Nov 11 14:15:11 2009 +0100 @@ -5,5 +5,5 @@ Root file for the SET protocol proofs. *) -no_document use_thy "Nat_Int_Bij"; +no_document use_thys ["Nat_Int_Bij"]; use_thys ["Cardholder_Registration", "Merchant_Registration", "Purchase"];