author | haftmann |
Sun, 16 Mar 2014 18:09:04 +0100 | |
changeset 56166 | 9a241bc276cd |
parent 54555 | e8c5e95d338b |
child 58814 | 4c0ad4162cb7 |
permissions | -rw-r--r-- |
(* Title: HOL/Coinduction.thy Author: Johannes Hölzl, TU Muenchen Author: Dmitriy Traytel, TU Muenchen Copyright 2013 Coinduction method that avoids some boilerplate compared to coinduct. *) header {* Coinduction Method *} theory Coinduction imports Ctr_Sugar begin ML_file "Tools/coinduction.ML" setup Coinduction.setup end