src/HOL/Imperative_HOL/Ref.thy
changeset 81706 7beb0cf38292
parent 80914 d97fdabd9e2b
equal deleted inserted replaced
81705:53fea2ccab19 81706:7beb0cf38292
   282 code_printing constant ref' \<rightharpoonup> (Eval) "(fn/ ()/ =>/ Unsynchronized.ref/ _)"
   282 code_printing constant ref' \<rightharpoonup> (Eval) "(fn/ ()/ =>/ Unsynchronized.ref/ _)"
   283 code_printing constant Ref.lookup \<rightharpoonup> (SML) "(fn/ ()/ =>/ !/ _)"
   283 code_printing constant Ref.lookup \<rightharpoonup> (SML) "(fn/ ()/ =>/ !/ _)"
   284 code_printing constant Ref.update \<rightharpoonup> (SML) "(fn/ ()/ =>/ _/ :=/ _)"
   284 code_printing constant Ref.update \<rightharpoonup> (SML) "(fn/ ()/ =>/ _/ :=/ _)"
   285 code_printing constant "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" \<rightharpoonup> (SML) infixl 6 "="
   285 code_printing constant "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" \<rightharpoonup> (SML) infixl 6 "="
   286 
   286 
   287 code_reserved Eval Unsynchronized
   287 code_reserved (Eval) Unsynchronized
   288 
   288 
   289 
   289 
   290 text \<open>OCaml\<close>
   290 text \<open>OCaml\<close>
   291 
   291 
   292 code_printing type_constructor ref \<rightharpoonup> (OCaml) "_/ ref"
   292 code_printing type_constructor ref \<rightharpoonup> (OCaml) "_/ ref"
   294 code_printing constant ref' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ ref/ _)"
   294 code_printing constant ref' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ ref/ _)"
   295 code_printing constant Ref.lookup \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ !/ _)"
   295 code_printing constant Ref.lookup \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ !/ _)"
   296 code_printing constant Ref.update \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ _/ :=/ _)"
   296 code_printing constant Ref.update \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ _/ :=/ _)"
   297 code_printing constant "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" \<rightharpoonup> (OCaml) infixl 4 "="
   297 code_printing constant "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" \<rightharpoonup> (OCaml) infixl 4 "="
   298 
   298 
   299 code_reserved OCaml ref
   299 code_reserved (OCaml) ref
   300 
   300 
   301 
   301 
   302 text \<open>Haskell\<close>
   302 text \<open>Haskell\<close>
   303 
   303 
   304 code_printing type_constructor ref \<rightharpoonup> (Haskell) "Heap.STRef/ Heap.RealWorld/ _"
   304 code_printing type_constructor ref \<rightharpoonup> (Haskell) "Heap.STRef/ Heap.RealWorld/ _"