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.
adjusted examples
authornipkow
Fri, 07 Sep 2012 07:20:55 +0200
changeset 49188 22f7e7b68f50
parent 49187 6096da55d2d6
child 49189 3f85cd15a0cc
child 49191 3601bf546775
adjusted examples
src/HOL/IMP/Abs_Int1_const.thy file | annotate | diff | comparison | revisions
src/HOL/IMP/Abs_Int1_parity.thy file | annotate | diff | comparison | revisions
src/HOL/IMP/Abs_Int2_ivl.thy file | annotate | diff | comparison | revisions
src/HOL/IMP/Abs_Int3.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/IMP/Abs_Int1_const.thy	Thu Sep 06 08:59:50 2012 -0700
+++ b/src/HOL/IMP/Abs_Int1_const.thy	Fri Sep 07 07:20:55 2012 +0200
@@ -89,6 +89,7 @@
 value "show_acom (steps test4_const 1)"
 value "show_acom (steps test4_const 2)"
 value "show_acom (steps test4_const 3)"
+value "show_acom (steps test4_const 4)"
 value "show_acom_opt (AI_const test4_const)"
 
 value "show_acom (steps test5_const 0)"
@@ -97,6 +98,7 @@
 value "show_acom (steps test5_const 3)"
 value "show_acom (steps test5_const 4)"
 value "show_acom (steps test5_const 5)"
+value "show_acom (steps test5_const 6)"
 value "show_acom_opt (AI_const test5_const)"
 
 value "show_acom (steps test6_const 0)"
@@ -111,6 +113,8 @@
 value "show_acom (steps test6_const 9)"
 value "show_acom (steps test6_const 10)"
 value "show_acom (steps test6_const 11)"
+value "show_acom (steps test6_const 12)"
+value "show_acom (steps test6_const 13)"
 value "show_acom_opt (AI_const test6_const)"
 
 
--- a/src/HOL/IMP/Abs_Int1_parity.thy	Thu Sep 06 08:59:50 2012 -0700
+++ b/src/HOL/IMP/Abs_Int1_parity.thy	Fri Sep 07 07:20:55 2012 +0200
@@ -136,6 +136,7 @@
 value "show_acom (steps test2_parity 3)"
 value "show_acom (steps test2_parity 4)"
 value "show_acom (steps test2_parity 5)"
+value "show_acom (steps test2_parity 6)"
 value "show_acom_opt (AI_parity test2_parity)"
 
 
--- a/src/HOL/IMP/Abs_Int2_ivl.thy	Thu Sep 06 08:59:50 2012 -0700
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Fri Sep 07 07:20:55 2012 +0200
@@ -261,6 +261,7 @@
 value "show_acom (steps test2_ivl 0)"
 value "show_acom (steps test2_ivl 1)"
 value "show_acom (steps test2_ivl 2)"
+value "show_acom (steps test2_ivl 3)"
 
 text{* Fixed point reached in 2 steps.
  Not so if the start value of x is known: *}
@@ -271,6 +272,7 @@
 value "show_acom (steps test3_ivl 2)"
 value "show_acom (steps test3_ivl 3)"
 value "show_acom (steps test3_ivl 4)"
+value "show_acom (steps test3_ivl 5)"
 
 text{* Takes as many iterations as the actual execution. Would diverge if
 loop did not terminate. Worse still, as the following example shows: even if
--- a/src/HOL/IMP/Abs_Int3.thy	Thu Sep 06 08:59:50 2012 -0700
+++ b/src/HOL/IMP/Abs_Int3.thy	Fri Sep 07 07:20:55 2012 +0200
@@ -395,9 +395,13 @@
 value "show_acom (step_up_ivl 3 (bot test3_ivl))"
 value "show_acom (step_up_ivl 4 (bot test3_ivl))"
 value "show_acom (step_up_ivl 5 (bot test3_ivl))"
-value "show_acom (step_down_ivl 1 (step_up_ivl 5 (bot test3_ivl)))"
-value "show_acom (step_down_ivl 2 (step_up_ivl 5 (bot test3_ivl)))"
-value "show_acom (step_down_ivl 3 (step_up_ivl 5 (bot test3_ivl)))"
+value "show_acom (step_up_ivl 6 (bot test3_ivl))"
+value "show_acom (step_up_ivl 7 (bot test3_ivl))"
+value "show_acom (step_up_ivl 8 (bot test3_ivl))"
+value "show_acom (step_down_ivl 1 (step_up_ivl 8 (bot test3_ivl)))"
+value "show_acom (step_down_ivl 2 (step_up_ivl 8 (bot test3_ivl)))"
+value "show_acom (step_down_ivl 3 (step_up_ivl 8 (bot test3_ivl)))"
+value "show_acom (step_down_ivl 4 (step_up_ivl 8 (bot test3_ivl)))"
 value "show_acom_opt (AI_ivl' test3_ivl)"
isabelle