| changeset 38797 | abe92b33ac9f |
| parent 38764 | e6a18808873c |
| child 42361 | 23f352990944 |
--- a/src/HOL/Tools/Function/measure_functions.ML Fri Aug 27 10:57:32 2010 +0200 +++ b/src/HOL/Tools/Function/measure_functions.ML Fri Aug 27 12:57:55 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 =