Re: [isabelle-dev] NEWS / CONTRIBUTORS

2011-09-12 Thread Florian Haftmann
Hi Lukas, the rename AssocList ~> AList_Impl should sound AssocList ~> AList Nota bene: T.thy – theory as intended to be used by other theoreis T_Impl.thy – implementation for abstract type Since ALists are not abstract, there is no AList_Impl.thy, but cf. RBT_Impl.thy. The rename

Re: [isabelle-dev] Option raised errors hides other error failures

2011-09-12 Thread Makarius
On Mon, 12 Sep 2011, Lukas Bulwahn wrote: In the concrete situation, above one needs to isolate the true reason for the unexpected non-determinism. Either by bisection over the history (induction over the construction of the sources) or by investigating the current version at runtime, with To

Re: [isabelle-dev] Option raised errors hides other error failures

2011-09-12 Thread Lukas Bulwahn
On 09/09/2011 02:52 PM, Makarius wrote: On Fri, 9 Sep 2011, Lukas Bulwahn wrote: In my concrete case: When running the compilation within the make command, I get: *** exception Option raised Exception- TOPLEVEL_ERROR raised *** ML error Whereas running it interactively in PG: *** exception

Re: [isabelle-dev] NEWS / CONTRIBUTORS

2011-09-12 Thread Lukas Bulwahn
Thanks for your pointer, Brian. Code_Char_ord.thy is documented under Code generation. I added NEWS and CONTRIBUTORS for Cset_Monad, Dlist_Cset, List_Cset, RBT_Mapping. Lukas On 09/11/2011 10:39 PM, Brian Huffman wrote: On Sun, Sep 11, 2011 at 1:01 PM, Makarius wrote: My impression is tha