turned fast_arith_split/neq_limit into configuration options;
authorwenzelm
Tue Jul 31 00:56:31 2007 +0200 (2007-07-31)
changeset 2407804b28c723d43
parent 24077 e7ba448bc571
child 24079 3ba5d68e076b
turned fast_arith_split/neq_limit into configuration options;
src/HOL/HoareParallel/Graph.thy
src/HOL/MicroJava/Comp/CorrCompTp.thy
     1.1 --- a/src/HOL/HoareParallel/Graph.thy	Tue Jul 31 00:56:31 2007 +0200
     1.2 +++ b/src/HOL/HoareParallel/Graph.thy	Tue Jul 31 00:56:31 2007 +0200
     1.3 @@ -173,9 +173,9 @@
     1.4   prefer 2 apply arith
     1.5   apply(drule_tac n = "Suc nata" in Compl_lemma)
     1.6   apply clarify
     1.7 - ML {* fast_arith_split_limit := 0; *}  (*FIXME*)
     1.8 + using [[option fast_arith_split_limit = 0]]
     1.9   apply force
    1.10 - ML {* fast_arith_split_limit := 9; *}  (*FIXME*)
    1.11 + using [[option fast_arith_split_limit = 9]]
    1.12  apply(drule leI)
    1.13  apply(subgoal_tac "Suc (length path - Suc m + nata)=(length path - Suc 0) - (m - Suc nata)")
    1.14   apply(erule_tac x = "m - (Suc nata)" in allE)
     2.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Tue Jul 31 00:56:31 2007 +0200
     2.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Tue Jul 31 00:56:31 2007 +0200
     2.3 @@ -454,10 +454,9 @@
     2.4  apply (simp add: max_of_list_def)
     2.5  apply (induct xs)
     2.6  apply simp
     2.7 -ML {* fast_arith_split_limit := 0; *}  (* FIXME *)
     2.8 +using [[option fast_arith_split_limit = 0]]
     2.9  apply simp
    2.10  apply arith
    2.11 -ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
    2.12  done
    2.13  
    2.14