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