[isabelle-dev] Word Libraries

[Makarius]

On 10/08/2021 17:34, Florian Haftmann wrote:
> Dear power users of the bit and word libraries,
> 
> I have finished polishing the bit and word material as envisaged before
> the next Isabelle release.

Is this failure a consequence of it? (Seen in current Isabelle/0f051404f487 +
AFP/bd6c4c7c76ec)

Native_Word FAILED
(see also
/Users/wenzelm/.isabelle/heaps/polyml-5.8.2_x86_64_32-darwin/log/Native_Word)
*** Type unification failed: Clash of types "_ ⇒ _" and "uint64"
***
*** Type error in application: operator not of function type
***
*** Operator:  x :: uint64
*** Operand:   AND :: ??'a
***
*** At command "lemma" (line 25 of "$AFP/Native_Word/Native_Word_Test_GHC.thy")
*** At command "test_code" (line 13 of
"$AFP/Native_Word/Native_Word_Test_GHC.thy")
*** Type unification failed: Clash of types "_ ⇒ _" and "uint64"
***
*** Type error in application: operator not of function type
***
*** Operator:  x :: uint64
*** Operand:   AND :: ??'a
***
*** At command "lemma" (line 25 of "$AFP/Native_Word/Native_Word_Test_GHC.thy")
Unfinished session(s): Native_Word


	Makarius