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