src/HOL/Coinduction.thy
author blanchet
Wed Nov 20 20:45:20 2013 +0100 (2013-11-20)
changeset 54540 5d7006e9205e
parent 54026 src/HOL/BNF/Coinduction.thy@82d9b2701a03
child 54555 e8c5e95d338b
permissions -rw-r--r--
moved 'coinduction' proof method to '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 Inductive
    13 begin
    14 
    15 ML_file "Tools/coinduction.ML"
    16 
    17 setup Coinduction.setup
    18 
    19 end