src/HOL/Induct/Com.thy
changeset 24178 4ff1dc2aa18d
parent 23746 a455e69c31cc
child 24824 b7866aea0815
     1.1 --- a/src/HOL/Induct/Com.thy	Tue Aug 07 20:19:54 2007 +0200
     1.2 +++ b/src/HOL/Induct/Com.thy	Tue Aug 07 20:19:55 2007 +0200
     1.3 @@ -93,10 +93,7 @@
     1.4    "((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> S)) = (R <= S)"
     1.5    by (auto simp add: le_fun_def le_bool_def)
     1.6  
     1.7 -ML {*
     1.8 -Unify.trace_bound := 30;
     1.9 -Unify.search_bound := 60;
    1.10 -*}
    1.11 +declare [[unify_trace_bound = 30, unify_search_bound = 60]]
    1.12  
    1.13  text{*Command execution is functional (deterministic) provided evaluation is*}
    1.14  theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"