src/HOL/ex/LSC_Examples.thy

--- a/src/HOL/ex/LSC_Examples.thy	Fri Mar 11 10:37:41 2011 +0100
+++ b/src/HOL/ex/LSC_Examples.thy	Fri Mar 11 10:37:42 2011 +0100
@@ -123,7 +123,8 @@
   "series_tree d = sum (cons ET) (apply (apply (apply (apply (cons MKT) series) series_tree) series_tree) series) d"
 by pat_completeness auto
 
-termination sorry
+termination proof (relation "measure nat_of")
+qed (auto simp add: of_int_inverse nat_of_def)
 
 instance ..