# HG changeset patch
# User krauss
# Date 1335724774 -7200
# Node ID 471cc845430b3d959c80f34bd42c37641564e910
# Parent  2d48bf79b7256416a395e854b9883443cfbf3d23
added test case for dependency graph (cf. 2d48bf79b725)

diff -r 2d48bf79b725 -r 471cc845430b src/HOL/ex/Termination.thy
--- a/src/HOL/ex/Termination.thy	Sun Apr 29 01:17:25 2012 +0200
+++ b/src/HOL/ex/Termination.thy	Sun Apr 29 20:39:34 2012 +0200
@@ -229,4 +229,21 @@
 by pat_completeness auto
 termination by size_change -- {* requires Multiset *}
 
+definition negate :: "int \<Rightarrow> int"
+where "negate i = - i"
+
+function fun3 :: "int => nat"
+where
+  "fun3 i =
+  (if i < 0 then fun3 (negate i)
+   else if i = 0 then 0
+   else fun3 (i - 1))"
+by (pat_completeness) auto
+termination
+  apply size_change
+  apply (simp add: negate_def)
+  apply size_change
+  done
+
+
 end