blanchet@54540: (*  Title:      HOL/Coinduction.thy
traytel@54026:     Author:     Johannes Hölzl, TU Muenchen
traytel@54026:     Author:     Dmitriy Traytel, TU Muenchen
traytel@54026:     Copyright   2013
traytel@54026: 
traytel@54026: Coinduction method that avoids some boilerplate compared to coinduct.
traytel@54026: *)
traytel@54026: 
traytel@54026: header {* Coinduction Method *}
traytel@54026: 
traytel@54026: theory Coinduction
blanchet@54555: imports Ctr_Sugar
traytel@54026: begin
traytel@54026: 
traytel@54026: ML_file "Tools/coinduction.ML"
traytel@54026: 
traytel@54026: setup Coinduction.setup
traytel@54026: 
traytel@54026: end