equal
deleted
inserted
replaced
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/ _" |