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
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
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
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