--- a/src/HOL/Library/Lattice_Syntax.thy Wed Jul 18 20:51:22 2018 +0200
+++ b/src/HOL/Library/Lattice_Syntax.thy Wed Jul 18 20:51:23 2018 +0200
@@ -3,7 +3,7 @@
section \<open>Pretty syntax for lattice operations\<close>
theory Lattice_Syntax
-imports HOL.Complete_Lattices
+imports Main
begin
notation
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy Wed Jul 18 20:51:22 2018 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Wed Jul 18 20:51:23 2018 +0200
@@ -7,7 +7,7 @@
*)
theory Quotient_Int
-imports "HOL-Library.Quotient_Product" HOL.Nat
+imports "HOL-Library.Quotient_Product"
begin
fun
--- a/src/HOL/ex/Computations.thy Wed Jul 18 20:51:22 2018 +0200
+++ b/src/HOL/ex/Computations.thy Wed Jul 18 20:51:23 2018 +0200
@@ -5,7 +5,7 @@
section \<open>Simple example for computations generated by the code generator\<close>
theory Computations
- imports HOL.Nat HOL.Fun_Def HOL.Num HOL.Code_Numeral
+ imports Main
begin
fun even :: "nat \<Rightarrow> bool"