Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
repaired reference implementation for OCaml
authorhaftmann
Wed, 14 Jul 2010 16:45:30 +0200
changeset 37830 01d308b00bcf
parent 37829 11f813e86305
child 37831 fa3a2e35c4f1
repaired reference implementation for OCaml
src/HOL/Imperative_HOL/Ref.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Imperative_HOL/Ref.thy	Wed Jul 14 16:45:30 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy	Wed Jul 14 16:45:30 2010 +0200
@@ -277,10 +277,10 @@
 text {* OCaml *}
 
 code_type ref (OCaml "_/ ref")
-code_const Ref (OCaml "failwith/ \"bare Ref\")")
-code_const ref (OCaml "(fn/ ()/ =>/ ref/ _)")
-code_const Ref.lookup (OCaml "(fn/ ()/ =>/ !/ _)")
-code_const Ref.update (OCaml "(fn/ ()/ =>/ _/ :=/ _)")
+code_const Ref (OCaml "failwith/ \"bare Ref\"")
+code_const ref (OCaml "(fun/ ()/ ->/ ref/ _)")
+code_const Ref.lookup (OCaml "(fun/ ()/ ->/ !/ _)")
+code_const Ref.update (OCaml "(fun/ ()/ ->/ _/ :=/ _)")
 
 code_reserved OCaml ref
isabelle