src/HOL/Induct/Com.thy
changeset 32367 a508148f7c25
parent 26806 40b411ec05aa
child 36862 952b2b102a0a
     1.1 --- a/src/HOL/Induct/Com.thy	Thu Aug 13 17:19:10 2009 +0100
     1.2 +++ b/src/HOL/Induct/Com.thy	Thu Aug 13 17:19:42 2009 +0100
     1.3 @@ -91,8 +91,6 @@
     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 mem_def)
     1.6  
     1.7 -declare [[unify_trace_bound = 30, unify_search_bound = 60]]
     1.8 -
     1.9  text{*Command execution is functional (deterministic) provided evaluation is*}
    1.10  theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"
    1.11  apply (simp add: single_valued_def)