src/HOL/Bali/Eval.thy
changeset 13462 56610e2ba220
parent 13384 a34e38154413
child 13601 fd3e3d6b37b2
     1.1 --- a/src/HOL/Bali/Eval.thy	Tue Aug 06 11:20:47 2002 +0200
     1.2 +++ b/src/HOL/Bali/Eval.thy	Tue Aug 06 11:22:05 2002 +0200
     1.3 @@ -894,7 +894,7 @@
     1.4    fun pred (_ $ (Const ("Pair",_) $ _ $ 
     1.5        (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ ))) $ _ ) = is_Inj x
     1.6  in
     1.7 -  make_simproc name lhs pred (thm name)
     1.8 +  cond_simproc name lhs pred (thm name)
     1.9  end
    1.10  
    1.11  val eval_expr_proc =eval_fun "expr" "In1l" "\<exists>v.  w=In1 v   \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<rightarrow> s'"
    1.12 @@ -989,7 +989,7 @@
    1.13       (Const ("Pair", _) $ x $ _) $ _ ) $ _)) = is_None x
    1.14  in
    1.15    val eval_no_abrupt_proc = 
    1.16 -  make_simproc "eval_no_abrupt" "G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')" pred 
    1.17 +  cond_simproc "eval_no_abrupt" "G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')" pred 
    1.18            (thm "eval_no_abrupt")
    1.19  end;
    1.20  Addsimprocs [eval_no_abrupt_proc]
    1.21 @@ -1017,7 +1017,7 @@
    1.22         x))) $ _ ) = is_Some x
    1.23  in
    1.24    val eval_abrupt_proc = 
    1.25 -  make_simproc "eval_abrupt" 
    1.26 +  cond_simproc "eval_abrupt" 
    1.27                 "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')" pred (thm "eval_abrupt")
    1.28  end;
    1.29  Addsimprocs [eval_abrupt_proc]