# HG changeset patch
# User wenzelm
# Date 1185836191 -7200
# Node ID 04b28c723d43eeff5c136831055d2fe2bdc9504a
# Parent  e7ba448bc571bca105a031ebcf81425a2533118b
turned fast_arith_split/neq_limit into configuration options;

diff -r e7ba448bc571 -r 04b28c723d43 src/HOL/HoareParallel/Graph.thy
--- a/src/HOL/HoareParallel/Graph.thy	Tue Jul 31 00:56:31 2007 +0200
+++ b/src/HOL/HoareParallel/Graph.thy	Tue Jul 31 00:56:31 2007 +0200
@@ -173,9 +173,9 @@
  prefer 2 apply arith
  apply(drule_tac n = "Suc nata" in Compl_lemma)
  apply clarify
- ML {* fast_arith_split_limit := 0; *}  (*FIXME*)
+ using [[option fast_arith_split_limit = 0]]
  apply force
- ML {* fast_arith_split_limit := 9; *}  (*FIXME*)
+ using [[option fast_arith_split_limit = 9]]
 apply(drule leI)
 apply(subgoal_tac "Suc (length path - Suc m + nata)=(length path - Suc 0) - (m - Suc nata)")
  apply(erule_tac x = "m - (Suc nata)" in allE)
diff -r e7ba448bc571 -r 04b28c723d43 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Tue Jul 31 00:56:31 2007 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Tue Jul 31 00:56:31 2007 +0200
@@ -454,10 +454,9 @@
 apply (simp add: max_of_list_def)
 apply (induct xs)
 apply simp
-ML {* fast_arith_split_limit := 0; *}  (* FIXME *)
+using [[option fast_arith_split_limit = 0]]
 apply simp
 apply arith
-ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
 done