diff -r 7ce5fcebfb35 -r a39ef48fbee0 src/HOL/Auth/Auth_Shared.thy
--- a/src/HOL/Auth/Auth_Shared.thy	Fri Apr 21 16:48:12 2017 +0200
+++ b/src/HOL/Auth/Auth_Shared.thy	Fri Apr 21 16:48:58 2017 +0200
@@ -6,22 +6,22 @@
 
 theory Auth_Shared
 imports
-  "NS_Shared"
-  "Kerberos_BAN"
-  "Kerberos_BAN_Gets"
-  "KerberosIV"
-  "KerberosIV_Gets"
-  "KerberosV"
-  "OtwayRees"
-  "OtwayRees_AN"
-  "OtwayRees_Bad"
-  "OtwayReesBella"
-  "WooLam"
-  "Recur"
-  "Yahalom"
-  "Yahalom2"
-  "Yahalom_Bad"
-  "ZhouGollmann"
+  NS_Shared
+  Kerberos_BAN
+  Kerberos_BAN_Gets
+  KerberosIV
+  KerberosIV_Gets
+  KerberosV
+  OtwayRees
+  OtwayRees_AN
+  OtwayRees_Bad
+  OtwayReesBella
+  WooLam
+  Recur
+  Yahalom
+  Yahalom2
+  Yahalom_Bad
+  ZhouGollmann
 begin
 
 end