[isabelle-dev] Isar syntax regression

I wonder whether then interpret Min!: semilattice_order_set min less_eq less. (without a space before the dot) is now intended Isar syntax. I found this in src/HOL/Big_Operators.thy, so I guess this is accepted in batch mode. PG doesn't accept it, but apparently JEdit does. Clemens

Re: [isabelle-dev] Shadowing of theorem names in locales

I recently tried to make HOL-Algebra compliant to this, but unfortunately got stuck in HOL already, where Big_Operators didn't comply either (but that's unlikely the only theory). If we are serious about forbidding duplicate theorem names eventually we probably need to start by introducing