# HG changeset patch
# User haftmann
# Date 1531939883 -7200
# Node ID 4ce18f389f53b89d699fc8d5a478c19821bb96ab
# Parent  db0c70767d86d13ac6d2ee849a6712431ed3b4d7
slightly more canonical imports

diff -r db0c70767d86 -r 4ce18f389f53 src/HOL/Library/Lattice_Syntax.thy
--- 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
diff -r db0c70767d86 -r 4ce18f389f53 src/HOL/Quotient_Examples/Quotient_Int.thy
--- 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
diff -r db0c70767d86 -r 4ce18f389f53 src/HOL/ex/Computations.thy
--- 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"