[isabelle-dev] NEWS: op <infix> -> (<infix>)

[Peter Lammich]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev