On Fri, 2012-09-07 at 17:20 +0200, Makarius wrote: > So when the code generator sees an interpreted function application > "loc.c t1 t2 t3 x y z" it should somehow do the right thing, in taking it as > "(loc.c t1 t2 t3) x y z", and considering the inner part as "atomic > entity" (and instance of c defined earlier in the abstract context).
I recently asked (somewhat clumsily, and not in the context of code generation) about essentially the same issue: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-August/msg00218.html So this is not restricted to code generation or simplification, but (unsurprisingly) also shows up in other applications. When there is a recommended way of doing the right thing here, I'd be grateful for a pointer. Best regards, Tjark _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
