# HG changeset patch
# User haftmann
# Date 1499535286 -7200
# Node ID 2b83dd24b301fae8294b96b5865bd5e341b07f9a
# Parent  3bc892346a6b1fbd4a4962957fb7f5914309ae7c
dropped superfluous theory imports

diff -r 3bc892346a6b -r 2b83dd24b301 src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Sat Jul 08 17:33:11 2017 +0200
+++ b/src/HOL/Library/State_Monad.thy	Sat Jul 08 19:34:46 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Combinator syntax for generic, open state monads (single-threaded monads)\<close>
 
 theory State_Monad
-imports Main Monad_Syntax
+imports Main
 begin
 
 subsection \<open>Motivation\<close>
diff -r 3bc892346a6b -r 2b83dd24b301 src/HOL/Proofs/Extraction/Euclid.thy
--- a/src/HOL/Proofs/Extraction/Euclid.thy	Sat Jul 08 17:33:11 2017 +0200
+++ b/src/HOL/Proofs/Extraction/Euclid.thy	Sat Jul 08 19:34:46 2017 +0200
@@ -10,6 +10,7 @@
 imports
   "~~/src/HOL/Computational_Algebra/Primes"
   Util
+  Old_Datatype
   "~~/src/HOL/Library/Code_Target_Numeral"
 begin
 
diff -r 3bc892346a6b -r 2b83dd24b301 src/HOL/Proofs/Extraction/Higman.thy
--- a/src/HOL/Proofs/Extraction/Higman.thy	Sat Jul 08 17:33:11 2017 +0200
+++ b/src/HOL/Proofs/Extraction/Higman.thy	Sat Jul 08 19:34:46 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>Higman's lemma\<close>
 
 theory Higman
-imports Old_Datatype
+imports Main
 begin
 
 text \<open>
diff -r 3bc892346a6b -r 2b83dd24b301 src/HOL/Proofs/Extraction/Higman_Extraction.thy
--- a/src/HOL/Proofs/Extraction/Higman_Extraction.thy	Sat Jul 08 17:33:11 2017 +0200
+++ b/src/HOL/Proofs/Extraction/Higman_Extraction.thy	Sat Jul 08 19:34:46 2017 +0200
@@ -6,7 +6,7 @@
 subsection \<open>Extracting the program\<close>
 
 theory Higman_Extraction
-imports Higman "~~/src/HOL/Library/State_Monad" Random
+imports Higman Old_Datatype "~~/src/HOL/Library/State_Monad"
 begin
 
 declare R.induct [ind_realizer]
diff -r 3bc892346a6b -r 2b83dd24b301 src/HOL/Proofs/Extraction/Pigeonhole.thy
--- a/src/HOL/Proofs/Extraction/Pigeonhole.thy	Sat Jul 08 17:33:11 2017 +0200
+++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy	Sat Jul 08 19:34:46 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>The pigeonhole principle\<close>
 
 theory Pigeonhole
-imports Util "~~/src/HOL/Library/Code_Target_Numeral"
+imports Util Old_Datatype "~~/src/HOL/Library/Code_Target_Numeral"
 begin
 
 text \<open>
diff -r 3bc892346a6b -r 2b83dd24b301 src/HOL/Proofs/Extraction/QuotRem.thy
--- a/src/HOL/Proofs/Extraction/QuotRem.thy	Sat Jul 08 17:33:11 2017 +0200
+++ b/src/HOL/Proofs/Extraction/QuotRem.thy	Sat Jul 08 19:34:46 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Quotient and remainder\<close>
 
 theory QuotRem
-imports Util
+imports Old_Datatype Util
 begin
 
 text \<open>Derivation of quotient and remainder using program extraction.\<close>
diff -r 3bc892346a6b -r 2b83dd24b301 src/HOL/Proofs/Extraction/Util.thy
--- a/src/HOL/Proofs/Extraction/Util.thy	Sat Jul 08 17:33:11 2017 +0200
+++ b/src/HOL/Proofs/Extraction/Util.thy	Sat Jul 08 19:34:46 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Auxiliary lemmas used in program extraction examples\<close>
 
 theory Util
-imports "~~/src/HOL/Library/Old_Datatype"
+imports Main
 begin
 
 text \<open>Decidability of equality on natural numbers.\<close>