Hi Isabelle people, esp. Makarius, it has come to my attention that attributes are called with a theory, a proof context and a local theory in this succession. Is this transforming the input lthy onion from inside out?
The implementation manual states that I have to treat all of them uniformly. This means that the attribute transformation on a lthy would not result in an update of the target context but of the auxilliary context instead. Is this correct and is the target guaranteed to be transformed in the same way beforehand? Also, does this mean we store the information resulting from attributes 3 times, namely in theories, contexts and local theories, potentially without any sharing? If in the process of a local theory transformation I want to store information to be looked up later, but not escaping the scope of the target, where should I store it? In the auxilliary context or the target context? Cheers, Andy _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
