src/HOL/Bali/State.thy
changeset 13524 604d0f3622d6
parent 13337 f75dfc606ac7
child 13688 a0b16d42d489
     1.1 --- a/src/HOL/Bali/State.thy	Tue Aug 27 11:03:02 2002 +0200
     1.2 +++ b/src/HOL/Bali/State.thy	Tue Aug 27 11:03:05 2002 +0200
     1.3 @@ -577,7 +577,7 @@
     1.4  apply auto
     1.5  done
     1.6  
     1.7 -lemma raise_if_SomeD [dest!]:
     1.8 +lemma error_if_SomeD [dest!]:
     1.9    "error_if c e y = Some z \<Longrightarrow> c \<and> z=(Error e) \<and> y=None \<or> (y=Some z)"
    1.10  apply (case_tac y)
    1.11  apply (case_tac c)
    1.12 @@ -773,7 +773,7 @@
    1.13   "\<not> (\<exists> err. x=Error err) \<Longrightarrow> error_free ((Some x),s)"
    1.14  by (auto simp add: error_free_def)
    1.15  
    1.16 -lemma error_free_absorb [simp,intro]: 
    1.17 +lemma error_free_abupd_absorb [simp,intro]: 
    1.18   "error_free s \<Longrightarrow> error_free (abupd (absorb j) s)"
    1.19  by (cases s) 
    1.20     (auto simp add: error_free_def absorb_def