Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dropped superfluous theory imports
authorhaftmann
Sat, 08 Jul 2017 19:34:46 +0200
changeset 66258 2b83dd24b301
parent 66257 3bc892346a6b
child 66259 b5279a21e658
dropped superfluous theory imports
src/HOL/Library/State_Monad.thy file | annotate | diff | comparison | revisions
src/HOL/Proofs/Extraction/Euclid.thy file | annotate | diff | comparison | revisions
src/HOL/Proofs/Extraction/Higman.thy file | annotate | diff | comparison | revisions
src/HOL/Proofs/Extraction/Higman_Extraction.thy file | annotate | diff | comparison | revisions
src/HOL/Proofs/Extraction/Pigeonhole.thy file | annotate | diff | comparison | revisions
src/HOL/Proofs/Extraction/QuotRem.thy file | annotate | diff | comparison | revisions
src/HOL/Proofs/Extraction/Util.thy file | annotate | diff | comparison | revisions 
--- 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>
--- 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
 
--- 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>
--- 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]
--- 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>
--- 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>
--- 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>
isabelle