[isabelle-dev] Auxiliary contexts again

Makarius makarius at sketis.net
Fri Oct 12 22:34:32 CEST 2012


Here are some leftovers from the last release concerning the nested 
auxiliary contexts:

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-June/msg00032.html
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-June/msg00052.html
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-June/msg00032.html

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-June/msg00045.html
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-June/msg00047.html
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-June/msg00035.html

The first three are should somehow work in Isabelle/18cb42182d3e, the 
others are still unclear.  Are there further issues still pending?


This is all from our National Debts department in some sense, and should 
at least become a bit better with every release.


 	Makarius


More information about the isabelle-dev mailing list