[isabelle-dev] Odd name space problem in quickcheck or codegen (due to change in typedef)

Makarius makarius at sketis.net
Thu Mar 3 14:16:10 CET 2016

On Thu, 3 Mar 2016, Florian Haftmann wrote:

> The matter turned out quite simple: a literal type constructor name has
> to be adjusted:
>> diff -r eef7af6af2ce thys/Native_Word/Uint32.thy
>> --- a/thys/Native_Word/Uint32.thy	Thu Mar 03 08:24:04 2016 +0100

Great. So I will push this change trough, with all the usual tests.


More information about the isabelle-dev mailing list