src/HOL/Coinduction.thy
author blanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58306 117ba6cbe414
parent 54555 e8c5e95d338b
child 58814 4c0ad4162cb7
permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
     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