src/HOL/Coinduction.thy
author blanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58306 117ba6cbe414
parent 54555 e8c5e95d338b
child 58814 4c0ad4162cb7
permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
blanchet@54540
     1
(*  Title:      HOL/Coinduction.thy
traytel@54026
     2
    Author:     Johannes Hölzl, TU Muenchen
traytel@54026
     3
    Author:     Dmitriy Traytel, TU Muenchen
traytel@54026
     4
    Copyright   2013
traytel@54026
     5
traytel@54026
     6
Coinduction method that avoids some boilerplate compared to coinduct.
traytel@54026
     7
*)
traytel@54026
     8
traytel@54026
     9
header {* Coinduction Method *}
traytel@54026
    10
traytel@54026
    11
theory Coinduction
blanchet@54555
    12
imports Ctr_Sugar
traytel@54026
    13
begin
traytel@54026
    14
traytel@54026
    15
ML_file "Tools/coinduction.ML"
traytel@54026
    16
traytel@54026
    17
setup Coinduction.setup
traytel@54026
    18
traytel@54026
    19
end