On 10/01/18 20:17, Tobias Nipkow wrote: > Invoking "isabelle > update_op" converts all files in the current directory (recursively). > In case you want to exclude conversion of ML files (because the tool > frequently also converts ML's "op" syntax), use option "-m". > > In revision eab6ce8368fa
These are more changes than I expected, but even that is to be expected with the wealth of material we have accumulated :-) BTW, in the follow-up change a82df75b7f85 ("tuned notation") the special breaks introduced by Larry in 1996 got lost: changeset: 2006:72754e060aa2 user: paulson date: Mon Sep 23 17:47:49 1996 +0200 files: src/HOL/Ord.thy src/HOL/Set.thy description: New infix syntax: breaks line BEFORE operator Larry has recently done analogous changes (e.g. bdf25939a550), so it appears to be still the state-of-the art to have these exceptions in pretty printing. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev