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.
tuned signature -- prefer Isabelle/ML structure Integer (despite minor confusion due to canonical argument order of "pow");
authorwenzelm
Fri, 01 Jan 2021 23:35:09 +0100
changeset 73021 f602a380e4f2
parent 73020 b51515722274
child 73022 38528017e4c8
tuned signature -- prefer Isabelle/ML structure Integer (despite minor confusion due to canonical argument order of "pow");
src/HOL/Library/Tools/smt_word.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Tools/smt_word.ML	Fri Jan 01 17:35:04 2021 +0100
+++ b/src/HOL/Library/Tools/smt_word.ML	Fri Jan 01 23:35:09 2021 +0100
@@ -42,7 +42,7 @@
   fun word_num (Type (\<^type_name>\<open>word\<close>, [T])) k =
         let
           val size = try dest_binT T
-          fun max_int size = IntInf.pow (2, size)
+          fun max_int size = Integer.pow size 2
         in
           (case size of
             NONE => NONE
isabelle