Quoting Makarius <makar...@sketis.net>:
Does it mean you propose to discontinue "(in a)" at some point?
Exactly. Too early right now, but eventually this might make sense -- especially if the IDE provides suitable refactorings. Of course, this wouldn't let us scrap a lot of code, but the Isar language could become cleaner.
Clemens _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
