| changeset 64430 | 1d85ac286c72 |
| parent 63655 | d31650b377c4 |
| child 69605 | a96320074298 |
--- a/src/HOL/Ctr_Sugar.thy Sat Oct 29 00:39:32 2016 +0200 +++ b/src/HOL/Ctr_Sugar.thy Sat Oct 29 00:39:33 2016 +0200 @@ -42,8 +42,8 @@ ML_file "Tools/Ctr_Sugar/ctr_sugar_code.ML" ML_file "Tools/Ctr_Sugar/ctr_sugar.ML" +text \<open>Coinduction method that avoids some boilerplate compared with coinduct.\<close> -text \<open>Coinduction method that avoids some boilerplate compared to coinduct.\<close> ML_file "Tools/coinduction.ML" end