src/HOL/Coinduction.thy
author wenzelm
Fri Mar 07 22:30:58 2014 +0100 (2014-03-07)
changeset 55990 41c6b99c5fb7
parent 54555 e8c5e95d338b
child 58814 4c0ad4162cb7
permissions -rw-r--r--
more antiquotations;
     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 setup Coinduction.setup
    18 
    19 end