--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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>
--- 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]
--- 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 {*