| changeset 41413 | 64cd30d6b0b8 | 
| parent 32632 | 8ae912371831 | 
--- a/src/HOL/Auth/ROOT.ML Wed Dec 29 13:51:17 2010 +0100 +++ b/src/HOL/Auth/ROOT.ML Wed Dec 29 17:34:41 2010 +0100 @@ -1,2 +1,7 @@ - -use_thys ["Auth_Shared", "Auth_Public", "Smartcard/Auth_Smartcard", "Guard/Auth_Guard_Shared", "Guard/Auth_Guard_Public"]; +use_thys [ + "Auth_Shared", + "Auth_Public", + "Smartcard/Auth_Smartcard", + "Guard/Auth_Guard_Shared", + "Guard/Auth_Guard_Public" +];