src/HOL/Coinduction.thy
author wenzelm
Wed Oct 29 11:33:29 2014 +0100 (2014-10-29)
changeset 58814 4c0ad4162cb7
parent 54555 e8c5e95d338b
child 58889 5b7a9633cfa8
permissions -rw-r--r--
modernized setup;
tuned whitespace;
     1 (*  Title:      HOL/Coinduction.thy
     2     Author:     Johannes Hölzl, TU Muenchen
     3     Author:     Dmitriy Traytel, TU Muenchen
     4     Copyright   2013
     5 
     6 Coinduction method that avoids some boilerplate compared to coinduct.
     7 *)
     8 
     9 header {* Coinduction Method *}
    10 
    11 theory Coinduction
    12 imports Ctr_Sugar
    13 begin
    14 
    15 ML_file "Tools/coinduction.ML"
    16 
    17 end