src/HOL/Coinduction.thy
author blanchet
Wed Feb 12 08:35:57 2014 +0100 (2014-02-12)
changeset 55415 05f5fdb8d093
parent 54555 e8c5e95d338b
child 58814 4c0ad4162cb7
permissions -rw-r--r--
renamed 'nat_{case,rec}' to '{case,rec}_nat'
     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