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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
