--- a/src/HOL/MicroJava/J/JTypeSafe.thy Thu Aug 13 17:19:10 2009 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Thu Aug 13 17:19:42 2009 +0100
@@ -183,8 +183,6 @@
(mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]))
*}
-declare [[unify_search_bound = 40, unify_trace_bound = 40]]
-
theorem eval_evals_exec_type_sound:
"wf_java_prog G ==>
@@ -368,8 +366,6 @@
done
-declare [[unify_search_bound = 20, unify_trace_bound = 20]]
-
lemma eval_type_sound: "!!E s s'.
[| wf_java_prog G; G\<turnstile>(x,s) -e\<succ>v -> (x',s'); (x,s)::\<preceq>E; E\<turnstile>e::T; G=prg E |]