equal
deleted
inserted
replaced
40 ML_file "Tools/Ctr_Sugar/ctr_sugar_util.ML" |
40 ML_file "Tools/Ctr_Sugar/ctr_sugar_util.ML" |
41 ML_file "Tools/Ctr_Sugar/ctr_sugar_tactics.ML" |
41 ML_file "Tools/Ctr_Sugar/ctr_sugar_tactics.ML" |
42 ML_file "Tools/Ctr_Sugar/ctr_sugar_code.ML" |
42 ML_file "Tools/Ctr_Sugar/ctr_sugar_code.ML" |
43 ML_file "Tools/Ctr_Sugar/ctr_sugar.ML" |
43 ML_file "Tools/Ctr_Sugar/ctr_sugar.ML" |
44 |
44 |
|
45 text \<open>Coinduction method that avoids some boilerplate compared with coinduct.\<close> |
45 |
46 |
46 text \<open>Coinduction method that avoids some boilerplate compared to coinduct.\<close> |
|
47 ML_file "Tools/coinduction.ML" |
47 ML_file "Tools/coinduction.ML" |
48 |
48 |
49 end |
49 end |