src/HOL/Coinduction.thy
changeset 54540 5d7006e9205e
parent 54026 82d9b2701a03
child 54555 e8c5e95d338b
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Coinduction.thy	Wed Nov 20 20:45:20 2013 +0100
     1.3 @@ -0,0 +1,19 @@
     1.4 +(*  Title:      HOL/Coinduction.thy
     1.5 +    Author:     Johannes Hölzl, TU Muenchen
     1.6 +    Author:     Dmitriy Traytel, TU Muenchen
     1.7 +    Copyright   2013
     1.8 +
     1.9 +Coinduction method that avoids some boilerplate compared to coinduct.
    1.10 +*)
    1.11 +
    1.12 +header {* Coinduction Method *}
    1.13 +
    1.14 +theory Coinduction
    1.15 +imports Inductive
    1.16 +begin
    1.17 +
    1.18 +ML_file "Tools/coinduction.ML"
    1.19 +
    1.20 +setup Coinduction.setup
    1.21 +
    1.22 +end