# HG changeset patch
# User wenzelm
# Date 1470861254 -7200
# Node ID d31650b377c45f6fde70b949569a72564b49ea1c
# Parent  f90e3926e627a957ce98a2a1bdd99053c5c15e34
simplified theory hierarchy;

diff -r f90e3926e627 -r d31650b377c4 src/HOL/Coinduction.thy
--- 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
diff -r f90e3926e627 -r d31650b377c4 src/HOL/Ctr_Sugar.thy
--- 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
diff -r f90e3926e627 -r d31650b377c4 src/HOL/Main.thy
--- 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>