--- a/src/HOL/Fun_Def.thy Sat Aug 16 19:01:31 2014 +0200
+++ b/src/HOL/Fun_Def.thy Sat Aug 16 19:20:11 2014 +0200
@@ -117,8 +117,8 @@
inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
where is_measure_trivial: "is_measure f"
+named_theorems measure_function "rules that guide the heuristic generation of measure functions"
ML_file "Tools/Function/measure_functions.ML"
-setup MeasureFunctions.setup
lemma measure_size[measure_function]: "is_measure size"
by (rule is_measure_trivial)