equal
deleted
inserted
replaced
129 "heap s aa = None \<Longrightarrow> \<forall>v::val. s:v \<ge> n \<longrightarrow> hupd(aa\<mapsto>obj) s:v \<ge> n" |
129 "heap s aa = None \<Longrightarrow> \<forall>v::val. s:v \<ge> n \<longrightarrow> hupd(aa\<mapsto>obj) s:v \<ge> n" |
130 apply (induct n) |
130 apply (induct n) |
131 apply auto |
131 apply auto |
132 apply (case_tac "aa=a") |
132 apply (case_tac "aa=a") |
133 apply auto |
133 apply auto |
134 apply (tactic "smp_tac @{context} 1 1") |
134 apply (tactic "smp_tac \<^context> 1 1") |
135 apply (case_tac "aa=a") |
135 apply (case_tac "aa=a") |
136 apply auto |
136 apply auto |
137 done |
137 done |
138 |
138 |
139 |
139 |