| changeset 58305 | 57752a91eec4 |
| parent 58002 | 0ed1e999a0fb |
| child 58377 | c6f93b8d2d8e |
--- a/src/HOL/Fun_Def.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Fun_Def.thy Thu Sep 11 18:54:36 2014 +0200 @@ -97,7 +97,7 @@ method_setup pat_completeness = {* Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac) -*} "prove completeness of datatype patterns" +*} "prove completeness of (co)datatype patterns" ML_file "Tools/Function/fun.ML" ML_file "Tools/Function/induction_schema.ML"