changeset 38764 | e6a18808873c |
parent 37678 | 0040bafffdef |
child 42361 | 23f352990944 |
--- a/src/HOL/Tools/Function/measure_functions.ML Thu Aug 26 20:42:09 2010 +0200 +++ b/src/HOL/Tools/Function/measure_functions.ML Thu Aug 26 21:04:22 2010 +0200 @@ -20,7 +20,7 @@ ( val name = "measure_function" val description = - "Rules that guide the heuristic generation of measure functions" + "rules that guide the heuristic generation of measure functions" ); fun mk_is_measure t =