# HG changeset patch
# User nipkow
# Date 1316579175 -7200
# Node ID 21334181f82096c0e2f99b4231524f92cf7a0879
# Parent  4e3b999c62fa9f7c18fd26e6bb1d1bed6c608c10
added example

diff -r 4e3b999c62fa -r 21334181f820 src/HOL/IMP/AbsInt1_ivl.thy
--- a/src/HOL/IMP/AbsInt1_ivl.thy	Wed Sep 21 03:24:54 2011 +0200
+++ b/src/HOL/IMP/AbsInt1_ivl.thy	Wed Sep 21 06:26:15 2011 +0200
@@ -251,4 +251,10 @@
  DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
 value [code] "list_up(AI_ivl test4_ivl Top)"
 
+text{* Nontermination not detected: *}
+definition "test5_ivl =
+ ''x'' ::= N 0;
+ WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
+value [code] "list_up(AI_ivl test5_ivl Top)"
+
 end
diff -r 4e3b999c62fa -r 21334181f820 src/HOL/IMP/AbsInt2.thy
--- a/src/HOL/IMP/AbsInt2.thy	Wed Sep 21 03:24:54 2011 +0200
+++ b/src/HOL/IMP/AbsInt2.thy	Wed Sep 21 06:26:15 2011 +0200
@@ -143,5 +143,6 @@
 
 value [code] "list_up(AI_ivl' test3_ivl Top)"
 value [code] "list_up(AI_ivl' test4_ivl Top)"
+value [code] "list_up(AI_ivl' test5_ivl Top)"
 
 end