[isabelle-dev] Isar syntax regression

Clemens Ballarin ballarin at in.tum.de
Tue Jun 4 21:31:01 CEST 2013

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.


More information about the isabelle-dev mailing list