[isabelle-dev] "local_setup" and "Generic_Data"

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Mon Aug 9 11:29:01 CEST 2010

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))) *}


    declaration {* fn phi => Data.map (Integer.add 3) *}

do the trick.


More information about the isabelle-dev mailing list