Hi all,
> I was trying to make Nitpick more context-friendly and thought that
> "local_setup" and "Generic_Data" would be my friends. However, "local_setup"
> seems to do nothing -- the changes I perform to the data are coldly ignored.
> The little theory below shows illustrates what I mean:
> [...]
> local_setup {* Context.proof_map (Data.map (Integer.add 3)) *}
FYI. Florian has explained this to me live. For the record,
local_setup {* Local_Theory.target (Context.proof_map (Data.map
(Integer.add 3))) *}
or
declaration {* fn phi => Data.map (Integer.add 3) *}
do the trick.
Jasmin
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
