Re: [isabelle-dev] typedef (open) legacy

2012-10-05 Thread Makarius
On Thu, 4 Oct 2012, Florian Haftmann wrote: I think either option 3 or 4 would make sense, although I'd say 4 is preferable for a couple of reasons: First, it makes the implementation of typedef simpler. Second, it actually gives users more flexibility because if they want a set constant, they

Re: [isabelle-dev] strange behaviour with Z3 and smt method

2012-10-05 Thread Jasmin Christian Blanchette
Am 05.10.2012 um 10:47 schrieb Lukas Bulwahn: Solver z3: Z3 proof parser (line 87): unknown sort: Bool Although it is possible to work around it, it might be worthwhile to investigate. Thanks for the report. See 6279490e0438. Jasmin ___

Re: [isabelle-dev] An note on code generator bookkeeping and the code generator preprocessor [was: Locale interpretation with mixins]

2012-10-05 Thread Makarius
On Thu, 4 Oct 2012, Florian Haftmann wrote: The current infrastructure has only a preprocessor applied *after* the internal bookkeeping (for reasons I will explain in a separate, long promised mail), so this would add further complexity here. What sets the code generator apart from other

Re: [isabelle-dev] jedit Replace Find

2012-10-05 Thread Makarius
On Tue, 2 Oct 2012, Tobias Nipkow wrote: For example 03bc7afe8814 There is certainly not a general problem of jedit and JVM on Mac OS that covers all versions of the past and future. Funny things on Mac OS have happened before, but were sorted out at some point, by looking very closely which