# HG changeset patch
# User wenzelm
# Date 1492786138 -7200
# Node ID a39ef48fbee016c727fc671cb799a4e6bc3b3ec6
# Parent  7ce5fcebfb35cbe1cf4d4d691b2ee0a903d3227f
tuned imports;

diff -r 7ce5fcebfb35 -r a39ef48fbee0 src/HOL/Analysis/Conformal_Mappings.thy
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Fri Apr 21 16:48:12 2017 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Fri Apr 21 16:48:58 2017 +0200
@@ -5,7 +5,7 @@
 text\<open>Also Cauchy's residue theorem by Wenda Li (2016)\<close>
 
 theory Conformal_Mappings
-imports "Cauchy_Integral_Theorem"
+imports Cauchy_Integral_Theorem
 
 begin
 
diff -r 7ce5fcebfb35 -r a39ef48fbee0 src/HOL/Auth/Auth_Public.thy
--- a/src/HOL/Auth/Auth_Public.thy	Fri Apr 21 16:48:12 2017 +0200
+++ b/src/HOL/Auth/Auth_Public.thy	Fri Apr 21 16:48:58 2017 +0200
@@ -6,10 +6,10 @@
 
 theory Auth_Public
 imports
-  "NS_Public_Bad"
-  "NS_Public"
-  "TLS"
-  "CertifiedEmail"
+  NS_Public_Bad
+  NS_Public
+  TLS
+  CertifiedEmail
 begin
 
 end
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
diff -r 7ce5fcebfb35 -r a39ef48fbee0 src/HOL/Auth/Guard/Auth_Guard_Public.thy
--- a/src/HOL/Auth/Guard/Auth_Guard_Public.thy	Fri Apr 21 16:48:12 2017 +0200
+++ b/src/HOL/Auth/Guard/Auth_Guard_Public.thy	Fri Apr 21 16:48:58 2017 +0200
@@ -6,10 +6,10 @@
 
 theory Auth_Guard_Public
 imports
-  "P1"
-  "P2"
-  "Guard_NS_Public"
-  "Proto"
+  P1
+  P2
+  Guard_NS_Public
+  Proto
 begin
 
 end
diff -r 7ce5fcebfb35 -r a39ef48fbee0 src/HOL/Auth/Guard/Auth_Guard_Shared.thy
--- a/src/HOL/Auth/Guard/Auth_Guard_Shared.thy	Fri Apr 21 16:48:12 2017 +0200
+++ b/src/HOL/Auth/Guard/Auth_Guard_Shared.thy	Fri Apr 21 16:48:58 2017 +0200
@@ -6,8 +6,8 @@
 
 theory Auth_Guard_Shared
 imports
-  "Guard_OtwayRees"
-  "Guard_Yahalom"
+  Guard_OtwayRees
+  Guard_Yahalom
 begin
 
 end
diff -r 7ce5fcebfb35 -r a39ef48fbee0 src/HOL/Auth/Smartcard/Auth_Smartcard.thy
--- a/src/HOL/Auth/Smartcard/Auth_Smartcard.thy	Fri Apr 21 16:48:12 2017 +0200
+++ b/src/HOL/Auth/Smartcard/Auth_Smartcard.thy	Fri Apr 21 16:48:58 2017 +0200
@@ -6,8 +6,8 @@
 
 theory Auth_Smartcard
 imports
-  "ShoupRubin"
-  "ShoupRubinBella"
+  ShoupRubin
+  ShoupRubinBella
 begin
 
 end
diff -r 7ce5fcebfb35 -r a39ef48fbee0 src/HOL/Corec_Examples/Paper_Examples.thy
--- a/src/HOL/Corec_Examples/Paper_Examples.thy	Fri Apr 21 16:48:12 2017 +0200
+++ b/src/HOL/Corec_Examples/Paper_Examples.thy	Fri Apr 21 16:48:58 2017 +0200
@@ -9,7 +9,7 @@
 section \<open>Small Examples from the Paper ``Friends with Benefits''\<close>
 
 theory Paper_Examples
-imports "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/FSet" "Complex_Main"
+imports "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/FSet" Complex_Main
 begin
 
 section \<open>Examples from the introduction\<close>
diff -r 7ce5fcebfb35 -r a39ef48fbee0 src/HOL/MicroJava/Comp/CorrComp.thy
--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Fri Apr 21 16:48:12 2017 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Fri Apr 21 16:48:58 2017 +0200
@@ -5,7 +5,7 @@
 (* Compiler correctness statement and proof *)
 
 theory CorrComp
-imports "../J/JTypeSafe" "LemmasComp"
+imports "../J/JTypeSafe" LemmasComp
 begin
 
 declare wf_prog_ws_prog [simp add]
diff -r 7ce5fcebfb35 -r a39ef48fbee0 src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Apr 21 16:48:12 2017 +0200
+++ b/src/HOL/ROOT	Fri Apr 21 16:48:58 2017 +0200
@@ -194,7 +194,7 @@
 session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
   options [document_variants = document]
   theories [document = false]
-    "Less_False"
+    Less_False
     "~~/src/HOL/Library/Multiset"
     "~~/src/HOL/Number_Theory/Fib"
   theories
@@ -352,7 +352,7 @@
   *}
   theories
     (*Basic meta-theory*)
-    "UNITY_Main"
+    UNITY_Main
 
     (*Simple examples: no composition*)
     "Simple/Deadlock"
@@ -384,7 +384,7 @@
     "Comp/Client"
 
     (*obsolete*)
-    "ELT"
+    ELT
   document_files "root.tex"
 
 session "HOL-Unix" in Unix = HOL +
@@ -741,9 +741,9 @@
 
 session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" +
   theories
-    "Dining_Cryptographers"
-    "Koepf_Duermuth_Countermeasure"
-    "Measure_Not_CCC"
+    Dining_Cryptographers
+    Koepf_Duermuth_Countermeasure
+    Measure_Not_CCC
 
 session "HOL-Nominal" in Nominal = HOL +
   options [document = false]
@@ -1124,7 +1124,7 @@
     finite and infinite sequences.
   *}
   options [document = false]
-  theories "Abstraction"
+  theories Abstraction
 
 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
   description {*