--- a/src/HOL/Coinduction.thy Wed Aug 10 22:05:36 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(* Title: HOL/Coinduction.thy
- Author: Johannes Hölzl, TU Muenchen
- Author: Dmitriy Traytel, TU Muenchen
- Copyright 2013
-
-Coinduction method that avoids some boilerplate compared to coinduct.
-*)
-
-section \<open>Coinduction Method\<close>
-
-theory Coinduction
-imports Ctr_Sugar
-begin
-
-ML_file "Tools/coinduction.ML"
-
-end
--- a/src/HOL/Ctr_Sugar.thy Wed Aug 10 22:05:36 2016 +0200
+++ b/src/HOL/Ctr_Sugar.thy Wed Aug 10 22:34:14 2016 +0200
@@ -42,4 +42,8 @@
ML_file "Tools/Ctr_Sugar/ctr_sugar_code.ML"
ML_file "Tools/Ctr_Sugar/ctr_sugar.ML"
+
+text \<open>Coinduction method that avoids some boilerplate compared to coinduct.\<close>
+ML_file "Tools/coinduction.ML"
+
end
--- a/src/HOL/Main.thy Wed Aug 10 22:05:36 2016 +0200
+++ b/src/HOL/Main.thy Wed Aug 10 22:34:14 2016 +0200
@@ -1,7 +1,7 @@
section \<open>Main HOL\<close>
theory Main
-imports Predicate_Compile Quickcheck_Narrowing Extraction Coinduction Nitpick BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices
+imports Predicate_Compile Quickcheck_Narrowing Extraction Nitpick BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices
begin
text \<open>