Re: [isabelle] A note on recent renovations in session HOL-Word



Hi Gerwin,

> I think that is a good endeavour, there is indeed much that can be expressed more nicely these days. Keeping larger changes to after Isabelle2019 would be good.
> 
> For testing, I guess we are one of the biggest users of Word proofs, so it might make sense to have a look at https://github.com/seL4/l4v/ and run that for at least the ARM architecture settings. Of course this is on Isabelle2018. There is another round of material accumulated there that I was planning to contribute to the AFP Word entry before the Isabelle2019 release, but I will probably run out of time (project deadlines, haven’t even managed yet to test RC1) and have to move it to the next one.
> 
> Are your current HOL-Word changes already in RC1 or planned for RC2? Was there much impact on AFP.Word_Lib?

the changes are already there in RC1.  The impact on AFP entries is
minimal.  In fact the primary purpose of the reorganization was to
understand what the fundamental concepts are and group the material
accordingly.

> I’m also happy to help with testing later changes and be involved in the content evolution of HOL-Word.

My aim is to leave HOL-Word.Word more or less »as it is«, but basing it
on newly emerging theories; this would allow to gradually find out which
parts of HOL-Word.Word are obsolete for particular applications without
endangering those that still need it.

Cheers,
	Florian

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.