equal
deleted
inserted
replaced
908 (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin))) |
908 (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin))) |
909 | number_of_codegen _ _ _ _ _ _ _ = NONE; |
909 | number_of_codegen _ _ _ _ _ _ _ = NONE; |
910 *} |
910 *} |
911 |
911 |
912 setup {* [Codegen.add_codegen "number_of_codegen" number_of_codegen] *} |
912 setup {* [Codegen.add_codegen "number_of_codegen" number_of_codegen] *} |
|
913 |
|
914 quickcheck_params [default_type = int] |
913 |
915 |
914 |
916 |
915 (*Legacy ML bindings, but no longer the structure Int.*) |
917 (*Legacy ML bindings, but no longer the structure Int.*) |
916 ML |
918 ML |
917 {* |
919 {* |