I observed that "(=)" is hard to type in the default symbols setup, it will be folded to "\<subseteq>)" if immediate completion is on (A short informal poll in our group resulted that most of us have immediate completion on).
When trying to write parametricity lemmas in predicate-style (eg for lifting/transfer), you have to type "(=)" frequently. Is it possible to keep (= bound to \<subseteq>, but exclude it from immediate completion? -- Peter On Mi, 2018-01-10 at 20:17 +0100, Tobias Nipkow wrote: > * The "op <infix-op>" syntax for infix operators has been replaced by > "(<infix-op>)". If <infix-op> begins or ends with a "*", there needs > to > be a space between the "*" and the corresponding parenthesis. > INCOMPATIBILITY. > There is an Isabelle tool "update_op" that converts theory and ML > files > to the new syntax. Because it is based on regular expression > matching, > the result may need a bit of manual postprocessing. 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 > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel > le-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
