src/HOL/BNF/Coinduction.thy
changeset 56013 d64a4ef26edb
parent 56012 cfb21e03fe2a
parent 56008 30666a281ae3
child 56014 748778ac0ab8
     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