1.1 --- a/src/HOL/BNF/Coinduction.thy Thu Dec 05 17:52:12 2013 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,19 +0,0 @@
1.4 -(* Title: HOL/BNF/Coinduction.thy
1.5 - Author: Johannes Hölzl, TU Muenchen
1.6 - Author: Dmitriy Traytel, TU Muenchen
1.7 - Copyright 2013
1.8 -
1.9 -Coinduction method that avoids some boilerplate compared to coinduct.
1.10 -*)
1.11 -
1.12 -header {* Coinduction Method *}
1.13 -
1.14 -theory Coinduction
1.15 -imports BNF_Util
1.16 -begin
1.17 -
1.18 -ML_file "Tools/coinduction.ML"
1.19 -
1.20 -setup Coinduction.setup
1.21 -
1.22 -end