[isabelle-dev] NEWS: op <infix> -> (<infix>)
lammich at in.tum.de
Tue Mar 6 16:04:51 CET 2018
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
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
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
> be a space between the "*" and the corresponding parenthesis.
> There is an Isabelle tool "update_op" that converts theory and ML
> to the new syntax. Because it is based on regular expression
> the result may need a bit of manual postprocessing. Invoking
> 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
More information about the isabelle-dev