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.
fxied bug for OCaml bigints
authorhaftmann
Thu, 25 Jan 2007 09:32:35 +0100
changeset 22176 29ba33d58637
parent 22175 d9e3e4c30d6b
child 22177 515021e98684
fxied bug for OCaml bigints
src/HOL/Integ/IntArith.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Integ/IntArith.thy	Thu Jan 25 09:32:34 2007 +0100
+++ b/src/HOL/Integ/IntArith.thy	Thu Jan 25 09:32:35 2007 +0100
@@ -448,7 +448,7 @@
      and "IntInf.-/ (_,/ 1))")
   (OCaml "_"
      and "Big'_int.big'_int'_of'_int/ 0"
-     and "Big'_int.big'_int'_of'_int/ -1"
+     and "Big'_int.big'_int'_of'_int/ (-1)"
      and "!(_; _; failwith \"BIT\")"
      and "Big'_int.succ'_big'_int"
      and "Big'_int.pred'_big'_int")
isabelle