Re: [isabelle-dev] Issues with "interpretations"

2014-04-03 Thread Jasmin Blanchette
Hi Andreas, > > 4. If anybody has any ideas on how to address Scenario 3, please let me > > know! > I don't think that scenario 3 is the one to address. IMO the hooks should > behave as if they were executed in the name space of the datatype > declaration, so size is doing something sensible al

Re: [isabelle-dev] Consolidation of manual naming

2014-04-03 Thread Florian Haftmann
> Otherwise any reform of this little aministrative problem of Isabelle > repository versions is one of the build_doc command line: there is no > need to specify the session here, it could just name the > "document_variant" instead (but that would mean to rewrite the shell > script in Isabelle/Scal