--- a/src/HOL/Imperative_HOL/Ref.thy Fri Jan 01 11:27:29 2016 +0100
+++ b/src/HOL/Imperative_HOL/Ref.thy Fri Jan 01 14:44:52 2016 +0100
@@ -208,11 +208,11 @@
using assms by (rule effectE) (simp add: execute_simps)
lemma lookup_chain:
- "(!r \<guillemotright> f) = f"
+ "(!r \<then> f) = f"
by (rule Heap_eqI) (auto simp add: lookup_def execute_simps intro: execute_bind)
lemma update_change [code]:
- "r := e = change (\<lambda>_. e) r \<guillemotright> return ()"
+ "r := e = change (\<lambda>_. e) r \<then> return ()"
by (rule Heap_eqI) (simp add: change_def lookup_chain)
@@ -320,4 +320,3 @@
code_printing constant "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" \<rightharpoonup> (Scala) infixl 5 "=="
end
-