author | blanchet |
Wed, 30 Jul 2014 09:40:28 +0200 | |
changeset 57830 | 2d0f0d6fdf3e |
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