src/HOL/MicroJava/J/JTypeSafe.thy
changeset 24178 4ff1dc2aa18d
parent 23894 1a4167d761ac
child 27098 d89fb4ee7280
     1.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Tue Aug 07 20:19:54 2007 +0200
     1.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Tue Aug 07 20:19:55 2007 +0200
     1.3 @@ -182,10 +182,8 @@
     1.4  val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
     1.5    (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]))
     1.6  *}
     1.7 -ML{*
     1.8 -Unify.search_bound := 40;
     1.9 -Unify.trace_bound  := 40
    1.10 -*}
    1.11 +
    1.12 +declare [[unify_search_bound = 40, unify_trace_bound = 40]]
    1.13  
    1.14  
    1.15  theorem eval_evals_exec_type_sound: 
    1.16 @@ -369,10 +367,8 @@
    1.17  apply (simp (no_asm_simp))+ 
    1.18  
    1.19  done
    1.20 -ML{*
    1.21 -Unify.search_bound := 20;
    1.22 -Unify.trace_bound  := 20
    1.23 -*}
    1.24 +
    1.25 +declare [[unify_search_bound = 20, unify_trace_bound = 20]]
    1.26  
    1.27  
    1.28  lemma eval_type_sound: "!!E s s'.