Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added example
authornipkow
Wed, 21 Sep 2011 06:26:15 +0200
changeset 45020 21334181f820
parent 45019 4e3b999c62fa
child 45021 d16343c47fb8
added example
src/HOL/IMP/AbsInt1_ivl.thy file | annotate | diff | comparison | revisions
src/HOL/IMP/AbsInt2.thy file | annotate | diff | comparison | revisions 
--- 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
--- 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
isabelle