# HG changeset patch
# User nipkow
# Date 1327829634 -3600
# Node ID 66486acfa26a32f704896d100bf0bd826c8b4077
# Parent  10c18630612a71a0f2a96e116438366449f97016
tuned

diff -r 10c18630612a -r 66486acfa26a src/HOL/IMP/Abs_Int0_const.thy
--- a/src/HOL/IMP/Abs_Int0_const.thy	Fri Jan 27 17:02:08 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0_const.thy	Sun Jan 29 10:33:54 2012 +0100
@@ -72,6 +72,46 @@
 proof qed
 
 
+subsubsection "Tests"
+
+value "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test1_const))"
+value "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test1_const))"
+value "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test1_const))"
+value "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test1_const))"
+value "show_acom_opt (AI_const test1_const)"
+
+value "show_acom_opt (AI_const test2_const)"
+value "show_acom_opt (AI_const test3_const)"
+
+value "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test4_const))"
+value "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test4_const))"
+value "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test4_const))"
+value "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test4_const))"
+value "show_acom_opt (AI_const test4_const)"
+
+value "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test5_const))"
+value "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test5_const))"
+value "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test5_const))"
+value "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test5_const))"
+value "show_acom (((step_const \<top>)^^4) (\<bottom>\<^sub>c test5_const))"
+value "show_acom (((step_const \<top>)^^5) (\<bottom>\<^sub>c test5_const))"
+value "show_acom_opt (AI_const test5_const)"
+
+value "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test6_const))"
+value "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test6_const))"
+value "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test6_const))"
+value "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test6_const))"
+value "show_acom (((step_const \<top>)^^4) (\<bottom>\<^sub>c test6_const))"
+value "show_acom (((step_const \<top>)^^5) (\<bottom>\<^sub>c test6_const))"
+value "show_acom (((step_const \<top>)^^6) (\<bottom>\<^sub>c test6_const))"
+value "show_acom (((step_const \<top>)^^7) (\<bottom>\<^sub>c test6_const))"
+value "show_acom (((step_const \<top>)^^8) (\<bottom>\<^sub>c test6_const))"
+value "show_acom (((step_const \<top>)^^9) (\<bottom>\<^sub>c test6_const))"
+value "show_acom (((step_const \<top>)^^10) (\<bottom>\<^sub>c test6_const))"
+value "show_acom (((step_const \<top>)^^11) (\<bottom>\<^sub>c test6_const))"
+value "show_acom_opt (AI_const test6_const)"
+
+
 text{* Monotonicity: *}
 
 interpretation Abs_Int_mono
@@ -96,32 +136,4 @@
 lemma "EX c'. AI_const c = Some c'"
 by(rule AI_Some_measure[OF measure_const measure_const_eq])
 
-
-subsubsection "Tests"
-
-value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test1_const))"
-value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test1_const))"
-value [code] "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test1_const))"
-value [code] "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test1_const))"
-value [code] "show_acom_opt (AI_const test1_const)"
-
-value [code] "show_acom_opt (AI_const test2_const)"
-value [code] "show_acom_opt (AI_const test3_const)"
-
-value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test4_const))"
-value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test4_const))"
-value [code] "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test4_const))"
-value [code] "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test4_const))"
-value [code] "show_acom_opt (AI_const test4_const)"
-
-value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test5_const))"
-value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test5_const))"
-value [code] "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test5_const))"
-value [code] "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test5_const))"
-value [code] "show_acom (((step_const \<top>)^^4) (\<bottom>\<^sub>c test5_const))"
-value [code] "show_acom (((step_const \<top>)^^5) (\<bottom>\<^sub>c test5_const))"
-value [code] "show_acom_opt (AI_const test5_const)"
-
-value [code] "show_acom_opt (AI_const test6_const)"
-
 end