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