# HG changeset patch
# User nipkow
# Date 1369175436 -7200
# Node ID 0c21dffc177ab9704f21c22cf833fb28a54ebf52
# Parent  090a519982e9568672590787f629f8ab92da3158
tuned

diff -r 090a519982e9 -r 0c21dffc177a src/HOL/IMP/Abs_Int_Tests.thy
--- a/src/HOL/IMP/Abs_Int_Tests.thy	Tue May 21 21:05:10 2013 +0200
+++ b/src/HOL/IMP/Abs_Int_Tests.thy	Wed May 22 00:30:36 2013 +0200
@@ -47,7 +47,7 @@
  DO ''x'' ::= Plus (V ''x'') (N 1)"
 
 definition "test3_ivl =
- ''x'' ::= N 7;;
+ ''x'' ::= N 0;;
  WHILE Less (V ''x'') (N 100)
  DO ''x'' ::= Plus (V ''x'') (N 1)"
 
@@ -58,7 +58,7 @@
 
 definition "test5_ivl =
  ''x'' ::= N 0;; ''y'' ::= N 0;;
- WHILE Less (V ''x'') (N 1000)
+ WHILE Less (V ''x'') (N 100)
  DO (''y'' ::= V ''x'';; ''x'' ::= Plus (V ''x'') (N 1))"
 
 definition "test6_ivl =