Am 04.06.2013 21:31, schrieb Clemens Ballarin:
> I wonder whether
>
> then interpret Min!: semilattice_order_set min less_eq less.
>
> (without a space before the dot) is now intended Isar syntax.
This concrete instance is definitely just a slip by myself.
Florian
--
PGP available:
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
___
