Manual updates towards conversion of "op" syntax
authornipkow
Wed Jan 10 15:21:49 2018 +0100 (17 months ago)
changeset 673985eb932e604a2
parent 67397 12b0c11e3d20
child 67399 eab6ce8368fa
Manual updates towards conversion of "op" syntax
NEWS
lib/Tools/update_op
src/Doc/Isar_Ref/Inner_Syntax.thy
src/Doc/Locales/Examples.thy
src/Doc/Locales/Examples3.thy
src/Doc/Tutorial/Documents/Documents.thy
src/HOL/Algebra/Ring.thy
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Preorder.thy
src/HOL/Orderings.thy
src/HOL/Set.thy
src/Pure/Syntax/mixfix.ML
src/ZF/ex/Ring.thy
     1.1 --- a/NEWS	Wed Jan 10 13:35:56 2018 +0100
     1.2 +++ b/NEWS	Wed Jan 10 15:21:49 2018 +0100
     1.3 @@ -9,6 +9,15 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* The "op <infix-op>" syntax for infix opertors has been replaced by
     1.8 +"(<infix-op>)". INCOMPATIBILITY.
     1.9 +There is an Isabelle tool "update_op" that converts theory and ML files
    1.10 +to the new syntax. Because it is based on regular expression matching,
    1.11 +the result may need a bit of manual postprocessing. Invoking "isabelle
    1.12 +update_op" converts all files in the current directory (recursively).
    1.13 +In case you want to exclude conversion of ML files (because the tool
    1.14 +frequently also converts ML's "op" syntax), use option "-m".
    1.15 +
    1.16  * The old 'def' command has been discontinued (legacy since
    1.17  Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
    1.18  object-logic equality or equivalence.
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/lib/Tools/update_op	Wed Jan 10 15:21:49 2018 +0100
     2.3 @@ -0,0 +1,97 @@
     2.4 +#!/usr/bin/env bash
     2.5 +#
     2.6 +# Author: Tobias Nipkow, TU Muenchen
     2.7 +#
     2.8 +# DESCRIPTION: update "op _" syntax
     2.9 +
    2.10 +## diagnostics
    2.11 +
    2.12 +function usage()
    2.13 +{
    2.14 +  echo
    2.15 +  echo "Usage: isabelle $PRG [OPTIONS] [DIR]"
    2.16 +  echo
    2.17 +  echo "  Options are:"
    2.18 +  echo "    -m           ignore .ML files"
    2.19 +  echo
    2.20 +  echo "  Update the old \"op _\" syntax in theory and ML files."
    2.21 +  echo
    2.22 +  exit 1
    2.23 +}
    2.24 +
    2.25 +
    2.26 +IGNORE_ML=""
    2.27 +
    2.28 +while getopts "m" OPT
    2.29 +do
    2.30 +  case "$OPT" in
    2.31 +    m)
    2.32 +      IGNORE_ML="true"
    2.33 +      ;;
    2.34 +    \?)
    2.35 +      usage
    2.36 +      ;;
    2.37 +  esac
    2.38 +done
    2.39 +
    2.40 +shift $(($OPTIND - 1))
    2.41 +
    2.42 +DIR="."
    2.43 +if [ -n "$1" ]; then
    2.44 +  DIR="$1"
    2.45 +fi
    2.46 +
    2.47 +read -r -d '' THY_SCRIPT <<'EOF'
    2.48 +# op [^]\<^bsub>*\<^esub> -> ([^]\<^bsub>*\<^esub>)
    2.49 +s/\([^a-zA-Z0-9_?']\)op [ ]*\(\[\^\]\\<\^bsub>[^\\]*\\<\^esub>\)/\1(\2)/g
    2.50 +# op *XY -> ( *XY)
    2.51 +s/\([^a-zA-Z0-9_?']\)op[ ]*\*\([a-zA-Z][a-zA-Z]\)/\1( \*\2)/g
    2.52 +# op *X -> ( *X)
    2.53 +s/\([^a-zA-Z0-9_?']\)op[ ]*\*\([a-zA-Z]\)/\1( \*\2)/g
    2.54 +# op *R -> ( *R)
    2.55 +s/\([^a-zA-Z0-9_?']\)op[ ]*\(\*\\<^sub>[a-zA-Z]\)/\1( \2)/g
    2.56 +# op *\<cdot> -> ( *\<cdot>)
    2.57 +s/\([^a-zA-Z0-9_?']\)op[ ]*\(\*\\<cdot>\)/\1( \2)/g
    2.58 +# op ** -> ( ** )
    2.59 +s/\([^a-zA-Z0-9_?']\)op[ ]*\*\*/\1( \*\* )/g
    2.60 +# op * -> ( * )
    2.61 +s/\([^a-zA-Z0-9_?']\)op[ ]*\*/\1( \* )/g
    2.62 +# (op +) -> (+)
    2.63 +s/(op [ ]*\([^ )("][^ )(",]*\))/(\1)/g
    2.64 +# (op + -> ((+)
    2.65 +s/(op [ ]*\([^ )(",]*\)\([^)]\)/((\1)\2/g
    2.66 +# op + -> (+)
    2.67 +s/\([^a-zA-Z0-9_?']\)op [ ]*\([^ )(",:]*\)::/\1(\2)::/g
    2.68 +s/\([^a-zA-Z0-9_?']\)op [ ]*\([^ )(",]*\)/\1(\2)/g
    2.69 +# op+ -> (+)
    2.70 +s/\([^a-zA-Z0-9_?']\)op\(\\<[a-zA-Z0-9]*>\)/\1(\2)/g
    2.71 +s/\([^a-zA-Z0-9_?']\)op\([^a-zA-Z0-9_? )("\][^ )(",:]*\)::/\1(\2)::/g
    2.72 +s/\([^a-zA-Z0-9_?']\)op\([^a-zA-Z0-9_? )("\][^ )(",]*\)/\1(\2)/g
    2.73 +EOF
    2.74 +
    2.75 +read -r -d '' ML_SCRIPT <<'EOF'
    2.76 +# op * -> ( * )
    2.77 +s/"\(.*\)\([^a-zA-Z0-9_]\)op[ ]*\*/"\1\2( \* )/g
    2.78 +s/"op[ ]*\*/"( \* )/g
    2.79 +# (op +) -> (+)
    2.80 +s/"\(.*\)(op [ ]*\([^ )("][^ )("]*\))/"\1(\2)/g
    2.81 +s/(op [ ]*\([^ )("][^ )("]*\))\(.*\)"/(\1)\2"/g
    2.82 +# (op + -> ((+)
    2.83 +s/"\(.*\)(op [ ]*\([^ )("]*\)\([^)]\)/"\1((\2)\3/g
    2.84 +# op + -> (+)
    2.85 +s/"\(.*\)\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)/"\1\2(\3)/g
    2.86 +s/"op [ ]*\([^ )("]*\)/"(\1)/g
    2.87 +# op+ -> (+)
    2.88 +s/"\(.*\)\([^a-zA-Z0-9_]\)op\([^a-zA-Z0-9_ )("][^ )("]*\)/"\1\2(\3)/g
    2.89 +s/"op\([^a-zA-Z0-9_ )("][^ )("]*\)/"(\1)/g
    2.90 +# is there \<...\> on the line (indicating Isabelle source):
    2.91 +s/\\<\([^>]*\)>\(.*\)\([^a-zA-Z0-9_]\)op \*/\\<\1>\2\3( * )/g
    2.92 +s/\\<\([^>]*\)>\(.*\)\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)\\<close>/\\<\1>\2\3(\4)\\<close>/g
    2.93 +s/\\<\([^>]*\)>\(.*\)\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)/\\<\1>\2\3(\4)/g
    2.94 +s/\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)\(.*\)\\<\([^>]*\)>/\1(\2)\3\\<\4>/g
    2.95 +EOF
    2.96 +
    2.97 +find "$DIR" -name "*.thy" -exec sed '-i~~' -e "$THY_SCRIPT" {} \;
    2.98 +
    2.99 +[ "$IGNORE_ML" = "true" ] || find "$DIR" -name "*.ML" -exec sed '-i~~' -e "$ML_SCRIPT" {} \;
   2.100 +
     3.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Wed Jan 10 13:35:56 2018 +0100
     3.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Wed Jan 10 15:21:49 2018 +0100
     3.3 @@ -439,9 +439,11 @@
     3.4    the delimiter is preceded by a space and followed by a space or line break;
     3.5    the entire phrase is a pretty printing block.
     3.6  
     3.7 -  The alternative notation \<^verbatim>\<open>op\<close>~\<open>sy\<close> is introduced in addition. Thus any
     3.8 -  infix operator may be written in prefix form (as in ML), independently of
     3.9 -  the number of arguments in the term.
    3.10 +  The alternative notation \<^verbatim>\<open>(\<close>\<open>sy\<close>\<^verbatim>\<open>)\<close> is introduced in addition. Thus any
    3.11 +  infix operator may be written in prefix form (as in Haskell), independently of
    3.12 +  the number of arguments in the term. To avoid conflict with the comment brackets
    3.13 +  \<^verbatim>\<open>(*\<close> and \<^verbatim>\<open>*)\<close>, infix operators that begin or end with a \<^verbatim>\<open>*\<close> require
    3.14 +  extra spaces, e.g. \<^verbatim>\<open>( * )\<close>.
    3.15  \<close>
    3.16  
    3.17  
    3.18 @@ -698,8 +700,8 @@
    3.19      & \<open>|\<close> & \<open>logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)  any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> & \<open>(999)\<close> \\
    3.20      & \<open>|\<close> & \<^verbatim>\<open>%\<close> \<open>pttrns\<close> \<^verbatim>\<open>.\<close> \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\
    3.21      & \<open>|\<close> & \<open>\<lambda>\<close> \<open>pttrns\<close> \<^verbatim>\<open>.\<close> \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\
    3.22 -    & \<open>|\<close> & \<^verbatim>\<open>op\<close> \<^verbatim>\<open>==\<close>~~\<open>|\<close>~~\<^verbatim>\<open>op\<close> \<open>\<equiv>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>op\<close> \<^verbatim>\<open>&&&\<close> \\
    3.23 -    & \<open>|\<close> & \<^verbatim>\<open>op\<close> \<^verbatim>\<open>==>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>op\<close> \<open>\<Longrightarrow>\<close> \\
    3.24 +    & \<open>|\<close> & \<^verbatim>\<open>(==)\<close>~~\<open>|\<close>~~\<^verbatim>\<open>(\<close>\<open>\<equiv>\<close>\<^verbatim>\<open>)\<close>~~\<open>|\<close>~~\<^verbatim>\<open>(&&&)\<close> \\
    3.25 +    & \<open>|\<close> & \<^verbatim>\<open>(==>)\<close>~~\<open>|\<close>~~\<^verbatim>\<open>(\<close>\<open>\<Longrightarrow>\<close>\<^verbatim>\<open>)\<close> \\
    3.26      & \<open>|\<close> & \<^verbatim>\<open>TYPE\<close> \<^verbatim>\<open>(\<close> \<open>type\<close> \<^verbatim>\<open>)\<close> \\\\
    3.27  
    3.28    @{syntax_def (inner) idt} & = & \<^verbatim>\<open>(\<close> \<open>idt\<close> \<^verbatim>\<open>)\<close>~~\<open>|  id  |\<close>~~\<^verbatim>\<open>_\<close> \\
     4.1 --- a/src/Doc/Locales/Examples.thy	Wed Jan 10 13:35:56 2018 +0100
     4.2 +++ b/src/Doc/Locales/Examples.thy	Wed Jan 10 15:21:49 2018 +0100
     4.3 @@ -77,7 +77,7 @@
     4.4  \begin{small}
     4.5  \begin{alltt}
     4.6    \isakeyword{fixes} le :: "'a \(\Rightarrow\) 'a \(\Rightarrow\)  bool" (\isakeyword{infixl} "\(\sqsubseteq\)" 50)
     4.7 -  \isakeyword{assumes} "partial_order op \(\sqsubseteq\)"
     4.8 +  \isakeyword{assumes} "partial_order (\(\sqsubseteq\))"
     4.9    \isakeyword{notes} assumption
    4.10      refl [intro, simp] = `?x \(\sqsubseteq\) ?x`
    4.11      \isakeyword{and}
     5.1 --- a/src/Doc/Locales/Examples3.thy	Wed Jan 10 13:35:56 2018 +0100
     5.2 +++ b/src/Doc/Locales/Examples3.thy	Wed Jan 10 15:21:49 2018 +0100
     5.3 @@ -5,9 +5,9 @@
     5.4  subsection \<open>Third Version: Local Interpretation
     5.5    \label{sec:local-interpretation}\<close>
     5.6  
     5.7 -text \<open>In the above example, the fact that @{term "op \<le>"} is a partial
     5.8 +text \<open>In the above example, the fact that @{term "(\<le>)"} is a partial
     5.9    order for the integers was used in the second goal to
    5.10 -  discharge the premise in the definition of @{text "op \<sqsubset>"}.  In
    5.11 +  discharge the premise in the definition of @{text "(\<sqsubset>)"}.  In
    5.12    general, proofs of the equations not only may involve definitions
    5.13    from the interpreted locale but arbitrarily complex arguments in the
    5.14    context of the locale.  Therefore it would be convenient to have the
    5.15 @@ -16,12 +16,12 @@
    5.16    The command for local interpretations is \isakeyword{interpret}.  We
    5.17    repeat the example from the previous section to illustrate this.\<close>
    5.18  
    5.19 -  interpretation %visible int: partial_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
    5.20 +  interpretation %visible int: partial_order "(\<le>) :: int \<Rightarrow> int \<Rightarrow> bool"
    5.21      rewrites "int.less x y = (x < y)"
    5.22    proof -
    5.23 -    show "partial_order (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
    5.24 +    show "partial_order ((\<le>) :: int \<Rightarrow> int \<Rightarrow> bool)"
    5.25        by unfold_locales auto
    5.26 -    then interpret int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool" .
    5.27 +    then interpret int: partial_order "(\<le>) :: [int, int] \<Rightarrow> bool" .
    5.28      show "int.less x y = (x < y)"
    5.29        unfolding int.less_def by auto
    5.30    qed
    5.31 @@ -46,11 +46,11 @@
    5.32    elaborate interpretation proof.  Note that the equations are named
    5.33    so they can be used in a later example.\<close>
    5.34  
    5.35 -  interpretation %visible int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
    5.36 +  interpretation %visible int: lattice "(\<le>) :: int \<Rightarrow> int \<Rightarrow> bool"
    5.37      rewrites int_min_eq: "int.meet x y = min x y"
    5.38        and int_max_eq: "int.join x y = max x y"
    5.39    proof -
    5.40 -    show "lattice (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
    5.41 +    show "lattice ((\<le>) :: int \<Rightarrow> int \<Rightarrow> bool)"
    5.42        txt \<open>\normalsize We have already shown that this is a partial
    5.43          order,\<close>
    5.44        apply unfold_locales
    5.45 @@ -68,17 +68,17 @@
    5.46      txt \<open>\normalsize In order to show the equations, we put ourselves
    5.47        in a situation where the lattice theorems can be used in a
    5.48        convenient way.\<close>
    5.49 -    then interpret int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" .
    5.50 +    then interpret int: lattice "(\<le>) :: int \<Rightarrow> int \<Rightarrow> bool" .
    5.51      show "int.meet x y = min x y"
    5.52        by (bestsimp simp: int.meet_def int.is_inf_def)
    5.53      show "int.join x y = max x y"
    5.54        by (bestsimp simp: int.join_def int.is_sup_def)
    5.55    qed
    5.56  
    5.57 -text \<open>Next follows that @{text "op \<le>"} is a total order, again for
    5.58 +text \<open>Next follows that @{text "(\<le>)"} is a total order, again for
    5.59    the integers.\<close>
    5.60  
    5.61 -  interpretation %visible int: total_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
    5.62 +  interpretation %visible int: total_order "(\<le>) :: int \<Rightarrow> int \<Rightarrow> bool"
    5.63      by unfold_locales arith
    5.64  
    5.65  text \<open>Theorems that are available in the theory at this point are shown in
    5.66 @@ -115,9 +115,9 @@
    5.67    the \isakeyword{sublocale} command.  Existing interpretations are
    5.68    skipped avoiding duplicate work.
    5.69  \item
    5.70 -  The predicate @{term "op <"} appears in theorem @{thm [source]
    5.71 +  The predicate @{term "(<)"} appears in theorem @{thm [source]
    5.72    int.less_total}
    5.73 -  although an equation for the replacement of @{text "op \<sqsubset>"} was only
    5.74 +  although an equation for the replacement of @{text "(\<sqsubset>)"} was only
    5.75    given in the interpretation of @{text partial_order}.  The
    5.76    interpretation equations are pushed downwards the hierarchy for
    5.77    related interpretations --- that is, for interpretations that share
    5.78 @@ -132,7 +132,7 @@
    5.79    outputs the following:
    5.80  \begin{small}
    5.81  \begin{alltt}
    5.82 -  int : partial_order "op \(\le\)"
    5.83 +  int : partial_order "(\(\le\))"
    5.84  \end{alltt}
    5.85  \end{small}
    5.86    Of course, there is only one interpretation.
    5.87 @@ -220,8 +220,8 @@
    5.88    \hspace*{1em}@{thm [source] le'.less_le_trans}:
    5.89    @{thm [display, indent=4] le'.less_le_trans}
    5.90    While there is infix syntax for the strict operation associated with
    5.91 -  @{term "op \<sqsubseteq>"}, there is none for the strict version of @{term
    5.92 -  "op \<preceq>"}.  The syntax @{text "\<sqsubset>"} for @{text less} is only
    5.93 +  @{term "(\<sqsubseteq>)"}, there is none for the strict version of @{term
    5.94 +  "(\<preceq>)"}.  The syntax @{text "\<sqsubset>"} for @{text less} is only
    5.95    available for the original instance it was declared for.  We may
    5.96    introduce infix syntax for @{text le'.less} with the following declaration:\<close>
    5.97  
    5.98 @@ -390,7 +390,7 @@
    5.99    certain conditions are fulfilled.  Take, for example, the function
   5.100    @{text "\<lambda>i. n * i"} that scales its argument by a constant factor.
   5.101    This function is order preserving (and even a lattice endomorphism)
   5.102 -  with respect to @{term "op \<le>"} provided @{text "n \<ge> 0"}.
   5.103 +  with respect to @{term "(\<le>)"} provided @{text "n \<ge> 0"}.
   5.104  
   5.105    It is not possible to express this using a global interpretation,
   5.106    because it is in general unspecified whether~@{term n} is
   5.107 @@ -412,14 +412,14 @@
   5.108    lattice endomorphisms.\<close>
   5.109  
   5.110    sublocale non_negative \<subseteq>
   5.111 -      order_preserving "op \<le>" "op \<le>" "\<lambda>i. n * i"
   5.112 +      order_preserving "(\<le>)" "(\<le>)" "\<lambda>i. n * i"
   5.113      using non_neg by unfold_locales (rule mult_left_mono)
   5.114  
   5.115  text \<open>While the proof of the previous interpretation
   5.116 -  is straightforward from monotonicity lemmas for~@{term "op *"}, the
   5.117 +  is straightforward from monotonicity lemmas for~@{term "( * )"}, the
   5.118    second proof follows a useful pattern.\<close>
   5.119  
   5.120 -  sublocale %visible non_negative \<subseteq> lattice_end "op \<le>" "\<lambda>i. n * i"
   5.121 +  sublocale %visible non_negative \<subseteq> lattice_end "(\<le>)" "\<lambda>i. n * i"
   5.122    proof (unfold_locales, unfold int_min_eq int_max_eq)
   5.123      txt \<open>\normalsize Unfolding the locale predicates \emph{and} the
   5.124        interpretation equations immediately yields two subgoals that
     6.1 --- a/src/Doc/Tutorial/Documents/Documents.thy	Wed Jan 10 13:35:56 2018 +0100
     6.2 +++ b/src/Doc/Tutorial/Documents/Documents.thy	Wed Jan 10 15:21:49 2018 +0100
     6.3 @@ -44,10 +44,10 @@
     6.4    \noindent Now @{text "xor A B"} and @{text "A [+] B"} refer to the
     6.5    same expression internally.  Any curried function with at least two
     6.6    arguments may be given infix syntax.  For partial applications with
     6.7 -  fewer than two operands, there is a notation using the prefix~@{text
     6.8 -  op}.  For instance, @{text xor} without arguments is represented as
     6.9 -  @{text "op [+]"}; together with ordinary function application, this
    6.10 -  turns @{text "xor A"} into @{text "op [+] A"}.
    6.11 +  fewer than two operands, the operator is enclosed in parentheses.
    6.12 +  For instance, @{text xor} without arguments is represented as
    6.13 +  @{text "([+])"}; together with ordinary function application, this
    6.14 +  turns @{text "xor A"} into @{text "([+]) A"}.
    6.15  
    6.16    The keyword \isakeyword{infixl} seen above specifies an
    6.17    infix operator that is nested to the \emph{left}: in iterated
     7.1 --- a/src/HOL/Algebra/Ring.thy	Wed Jan 10 13:35:56 2018 +0100
     7.2 +++ b/src/HOL/Algebra/Ring.thy	Wed Jan 10 15:21:49 2018 +0100
     7.3 @@ -22,7 +22,7 @@
     7.4    where "a_inv R = m_inv \<lparr>carrier = carrier R, mult = add R, one = zero R\<rparr>"
     7.5  
     7.6  definition
     7.7 -  a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
     7.8 +  a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" ("(_ \<ominus>\<index> _)" [65,66] 65)
     7.9    where "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
    7.10  
    7.11  locale abelian_monoid =
     8.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Jan 10 13:35:56 2018 +0100
     8.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Jan 10 15:21:49 2018 +0100
     8.3 @@ -394,12 +394,12 @@
     8.4  lemmas dlo_simps[no_atp] = order_refl less_irrefl not_less not_le exists_neq
     8.5    le_less neq_iff linear less_not_permute
     8.6  
     8.7 -lemma axiom[no_atp]: "class.unbounded_dense_linorder (op \<le>) (op <)"
     8.8 +lemma axiom[no_atp]: "class.unbounded_dense_linorder (\<le>) (<)"
     8.9    by (rule unbounded_dense_linorder_axioms)
    8.10  lemma atoms[no_atp]:
    8.11    shows "TERM (less :: 'a \<Rightarrow> _)"
    8.12      and "TERM (less_eq :: 'a \<Rightarrow> _)"
    8.13 -    and "TERM (op = :: 'a \<Rightarrow> _)" .
    8.14 +    and "TERM ((=) :: 'a \<Rightarrow> _)" .
    8.15  
    8.16  declare axiom[langford qe: dlo_qe_bnds dlo_qe_nolb dlo_qe_noub gather: gather_start gather_simps atoms: atoms]
    8.17  declare dlo_simps[langfordsimp]
    8.18 @@ -438,9 +438,9 @@
    8.19  begin
    8.20  
    8.21  notation
    8.22 -  less_eq  ("op \<sqsubseteq>") and
    8.23 +  less_eq  ("'(\<sqsubseteq>')") and
    8.24    less_eq  ("(_/ \<sqsubseteq> _)" [51, 51] 50) and
    8.25 -  less  ("op \<sqsubset>") and
    8.26 +  less  ("'(\<sqsubset>')") and
    8.27    less  ("(_/ \<sqsubset> _)"  [51, 51] 50)
    8.28  
    8.29  end
    8.30 @@ -705,7 +705,7 @@
    8.31  lemma atoms[no_atp]:
    8.32    shows "TERM (less :: 'a \<Rightarrow> _)"
    8.33      and "TERM (less_eq :: 'a \<Rightarrow> _)"
    8.34 -    and "TERM (op = :: 'a \<Rightarrow> _)" .
    8.35 +    and "TERM ((=) :: 'a \<Rightarrow> _)" .
    8.36  
    8.37  declare ferrack_axiom [ferrack minf: minf_thms pinf: pinf_thms
    8.38      nmi: nmi_thms npi: npi_thms lindense:
    8.39 @@ -716,7 +716,7 @@
    8.40    fun simps phi = map (Morphism.thm phi) [@{thm "not_less"}, @{thm "not_le"}]
    8.41    fun generic_whatis phi =
    8.42      let
    8.43 -      val [lt, le] = map (Morphism.term phi) [@{term "op \<sqsubset>"}, @{term "op \<sqsubseteq>"}]
    8.44 +      val [lt, le] = map (Morphism.term phi) [@{term "(\<sqsubset>)"}, @{term "(\<sqsubseteq>)"}]
    8.45        fun h x t =
    8.46          case Thm.term_of t of
    8.47            Const(@{const_name HOL.eq}, _)$y$z =>
    8.48 @@ -885,7 +885,7 @@
    8.49    using eq_diff_eq[where a= x and b=t and c=0] by simp
    8.50  
    8.51  interpretation class_dense_linordered_field: constr_dense_linorder
    8.52 -  "op \<le>" "op <" "\<lambda>x y. 1/2 * ((x::'a::linordered_field) + y)"
    8.53 +  "(\<le>)" "(<)" "\<lambda>x y. 1/2 * ((x::'a::linordered_field) + y)"
    8.54    by unfold_locales (dlo, dlo, auto)
    8.55  
    8.56  declaration \<open>
     9.1 --- a/src/HOL/Library/Multiset.thy	Wed Jan 10 13:35:56 2018 +0100
     9.2 +++ b/src/HOL/Library/Multiset.thy	Wed Jan 10 15:21:49 2018 +0100
     9.3 @@ -148,22 +148,22 @@
     9.4    where "Melem a M \<equiv> a \<in> set_mset M"
     9.5  
     9.6  notation
     9.7 -  Melem  ("op \<in>#") and
     9.8 +  Melem  ("'(\<in>#')") and
     9.9    Melem  ("(_/ \<in># _)" [51, 51] 50)
    9.10  
    9.11  notation  (ASCII)
    9.12 -  Melem  ("op :#") and
    9.13 +  Melem  ("'(:#')") and
    9.14    Melem  ("(_/ :# _)" [51, 51] 50)
    9.15  
    9.16  abbreviation not_Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"
    9.17    where "not_Melem a M \<equiv> a \<notin> set_mset M"
    9.18  
    9.19  notation
    9.20 -  not_Melem  ("op \<notin>#") and
    9.21 +  not_Melem  ("'(\<notin>#')") and
    9.22    not_Melem  ("(_/ \<notin># _)" [51, 51] 50)
    9.23  
    9.24  notation  (ASCII)
    9.25 -  not_Melem  ("op ~:#") and
    9.26 +  not_Melem  ("'(~:#')") and
    9.27    not_Melem  ("(_/ ~:# _)" [51, 51] 50)
    9.28  
    9.29  context
    9.30 @@ -533,11 +533,11 @@
    9.31    supseteq_mset  (infix ">=#" 50) and
    9.32    supset_mset  (infix ">#" 50)
    9.33  
    9.34 -interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op -" "op \<subseteq>#" "op \<subset>#"
    9.35 +interpretation subset_mset: ordered_ab_semigroup_add_imp_le "(+)" "(-)" "(\<subseteq>#)" "(\<subset>#)"
    9.36    by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
    9.37      \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
    9.38  
    9.39 -interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "op +" 0 "op -" "op \<subseteq>#" "op \<subset>#"
    9.40 +interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "(+)" 0 "(-)" "(\<subseteq>#)" "(\<subset>#)"
    9.41    by standard
    9.42      \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
    9.43  
    9.44 @@ -556,7 +556,7 @@
    9.45     apply (auto intro: multiset_eq_iff [THEN iffD2])
    9.46    done
    9.47  
    9.48 -interpretation subset_mset: ordered_cancel_comm_monoid_diff "op +" 0 "op \<subseteq>#" "op \<subset>#" "op -"
    9.49 +interpretation subset_mset: ordered_cancel_comm_monoid_diff "(+)" 0 "(\<subseteq>#)" "(\<subset>#)" "(-)"
    9.50    by standard (simp, fact mset_subset_eq_exists_conv)
    9.51      \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
    9.52  
    9.53 @@ -690,27 +690,27 @@
    9.54  definition inf_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "\<inter>#" 70) where
    9.55    multiset_inter_def: "inf_subset_mset A B = A - (A - B)"
    9.56  
    9.57 -interpretation subset_mset: semilattice_inf inf_subset_mset "op \<subseteq>#" "op \<subset>#"
    9.58 +interpretation subset_mset: semilattice_inf inf_subset_mset "(\<subseteq>#)" "(\<subset>#)"
    9.59  proof -
    9.60    have [simp]: "m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" for m n q :: nat
    9.61      by arith
    9.62 -  show "class.semilattice_inf op \<inter># op \<subseteq># op \<subset>#"
    9.63 +  show "class.semilattice_inf (\<inter>#) (\<subseteq>#) (\<subset>#)"
    9.64      by standard (auto simp add: multiset_inter_def subseteq_mset_def)
    9.65  qed \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
    9.66  
    9.67  definition sup_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"(infixl "\<union>#" 70)
    9.68    where "sup_subset_mset A B = A + (B - A)" \<comment> \<open>FIXME irregular fact name\<close>
    9.69  
    9.70 -interpretation subset_mset: semilattice_sup sup_subset_mset "op \<subseteq>#" "op \<subset>#"
    9.71 +interpretation subset_mset: semilattice_sup sup_subset_mset "(\<subseteq>#)" "(\<subset>#)"
    9.72  proof -
    9.73    have [simp]: "m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q - m) \<le> n" for m n q :: nat
    9.74      by arith
    9.75 -  show "class.semilattice_sup op \<union># op \<subseteq># op \<subset>#"
    9.76 +  show "class.semilattice_sup (\<union>#) (\<subseteq>#) (\<subset>#)"
    9.77      by standard (auto simp add: sup_subset_mset_def subseteq_mset_def)
    9.78  qed \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
    9.79  
    9.80 -interpretation subset_mset: bounded_lattice_bot "op \<inter>#" "op \<subseteq>#" "op \<subset>#"
    9.81 -  "op \<union>#" "{#}"
    9.82 +interpretation subset_mset: bounded_lattice_bot "(\<inter>#)" "(\<subseteq>#)" "(\<subset>#)"
    9.83 +  "(\<union>#)" "{#}"
    9.84    by standard auto
    9.85      \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
    9.86  
    9.87 @@ -1120,7 +1120,7 @@
    9.88    using assms by (simp add: Sup_multiset_def Abs_multiset_inverse Sup_multiset_in_multiset)
    9.89  
    9.90  
    9.91 -interpretation subset_mset: conditionally_complete_lattice Inf Sup "op \<inter>#" "op \<subseteq>#" "op \<subset>#" "op \<union>#"
    9.92 +interpretation subset_mset: conditionally_complete_lattice Inf Sup "(\<inter>#)" "(\<subseteq>#)" "(\<subset>#)" "(\<union>#)"
    9.93  proof
    9.94    fix X :: "'a multiset" and A
    9.95    assume "X \<in> A"
    9.96 @@ -1244,7 +1244,7 @@
    9.97    with assms show ?thesis by (simp add: in_Sup_multiset_iff)
    9.98  qed
    9.99  
   9.100 -interpretation subset_mset: distrib_lattice "op \<inter>#" "op \<subseteq>#" "op \<subset>#" "op \<union>#"
   9.101 +interpretation subset_mset: distrib_lattice "(\<inter>#)" "(\<subseteq>#)" "(\<subset>#)" "(\<union>#)"
   9.102  proof
   9.103    fix A B C :: "'a multiset"
   9.104    show "A \<union># (B \<inter># C) = A \<union># B \<inter># (A \<union># C)"
   9.105 @@ -2269,12 +2269,12 @@
   9.106  end
   9.107  end
   9.108  
   9.109 -lemma comp_fun_commute_plus_mset[simp]: "comp_fun_commute (op + :: 'a multiset \<Rightarrow> _ \<Rightarrow> _)"
   9.110 +lemma comp_fun_commute_plus_mset[simp]: "comp_fun_commute ((+) :: 'a multiset \<Rightarrow> _ \<Rightarrow> _)"
   9.111    by standard (simp add: add_ac comp_def)
   9.112  
   9.113  declare comp_fun_commute.fold_mset_add_mset[OF comp_fun_commute_plus_mset, simp]
   9.114  
   9.115 -lemma in_mset_fold_plus_iff[iff]: "x \<in># fold_mset (op +) M NN \<longleftrightarrow> x \<in># M \<or> (\<exists>N. N \<in># NN \<and> x \<in># N)"
   9.116 +lemma in_mset_fold_plus_iff[iff]: "x \<in># fold_mset (+) M NN \<longleftrightarrow> x \<in># M \<or> (\<exists>N. N \<in># NN \<and> x \<in># N)"
   9.117    by (induct NN) auto
   9.118  
   9.119  context comm_monoid_add
   9.120 @@ -2626,7 +2626,7 @@
   9.121    have "\<And>x P. P (f x) ?pivot \<and> f l = f x \<longleftrightarrow> P (f l) ?pivot \<and> f l = f x" by auto
   9.122    then have "\<And>P. [x \<leftarrow> sort_key f xs . P (f x) ?pivot \<and> f l = f x] =
   9.123      [x \<leftarrow> sort_key f xs. P (f l) ?pivot \<and> f l = f x]" by simp
   9.124 -  note *** = this [of "op <"] this [of "op >"] this [of "op ="]
   9.125 +  note *** = this [of "(<)"] this [of "(>)"] this [of "(=)"]
   9.126    show "[x \<leftarrow> ?rhs. f l = f x] = [x \<leftarrow> ?lhs. f l = f x]"
   9.127    proof (cases "f l" ?pivot rule: linorder_cases)
   9.128      case less
   9.129 @@ -2998,7 +2998,7 @@
   9.130  text \<open>
   9.131    Predicate variants of \<open>mult\<close> and the reflexive closure of \<open>mult\<close>, which are
   9.132    executable whenever the given predicate \<open>P\<close> is. Together with the standard
   9.133 -  code equations for \<open>op \<inter>#\<close> and \<open>op -\<close> this should yield quadratic
   9.134 +  code equations for \<open>(\<inter>#\<close>) and \<open>(-\<close>) this should yield quadratic
   9.135    (with respect to calls to \<open>P\<close>) implementations of \<open>multp\<close> and \<open>multeqp\<close>.
   9.136  \<close>
   9.137  
   9.138 @@ -3346,10 +3346,10 @@
   9.139            let
   9.140              val (maybe_opt, ps) =
   9.141                Nitpick_Model.dest_plain_fun t'
   9.142 -              ||> op ~~
   9.143 +              ||> (~~)
   9.144                ||> map (apsnd (snd o HOLogic.dest_number))
   9.145              fun elems_for t =
   9.146 -              (case AList.lookup (op =) ps t of
   9.147 +              (case AList.lookup (=) ps t of
   9.148                  SOME n => replicate n t
   9.149                | NONE => [Const (maybe_name, elem_T --> elem_T) $ t])
   9.150            in
   9.151 @@ -3438,7 +3438,7 @@
   9.152  
   9.153  fun subset_eq_mset_impl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool option" where
   9.154    "subset_eq_mset_impl [] ys = Some (ys \<noteq> [])"
   9.155 -| "subset_eq_mset_impl (Cons x xs) ys = (case List.extract (op = x) ys of
   9.156 +| "subset_eq_mset_impl (Cons x xs) ys = (case List.extract ((=) x) ys of
   9.157       None \<Rightarrow> None
   9.158     | Some (ys1,_,ys2) \<Rightarrow> subset_eq_mset_impl xs (ys1 @ ys2))"
   9.159  
   9.160 @@ -3451,7 +3451,7 @@
   9.161  next
   9.162    case (Cons x xs ys)
   9.163    show ?case
   9.164 -  proof (cases "List.extract (op = x) ys")
   9.165 +  proof (cases "List.extract ((=) x) ys")
   9.166      case None
   9.167      hence x: "x \<notin> set ys" by (simp add: extract_None_iff)
   9.168      {
   9.169 @@ -3510,8 +3510,8 @@
   9.170  qed
   9.171  
   9.172  text \<open>
   9.173 -  Exercise for the casual reader: add implementations for @{term "op \<le>"}
   9.174 -  and @{term "op <"} (multiset order).
   9.175 +  Exercise for the casual reader: add implementations for @{term "(\<le>)"}
   9.176 +  and @{term "(<)"} (multiset order).
   9.177  \<close>
   9.178  
   9.179  text \<open>Quickcheck generators\<close>
   9.180 @@ -3668,7 +3668,7 @@
   9.181      unfolding comp_def by (rule ext) (simp add: comp_def image_mset.compositionality)
   9.182    show "(\<And>z. z \<in> set_mset X \<Longrightarrow> f z = g z) \<Longrightarrow> image_mset f X = image_mset g X" for f g X
   9.183      by (induct X) simp_all
   9.184 -  show "set_mset \<circ> image_mset f = op ` f \<circ> set_mset" for f
   9.185 +  show "set_mset \<circ> image_mset f = (`) f \<circ> set_mset" for f
   9.186      by auto
   9.187    show "card_order natLeq"
   9.188      by (rule natLeq_card_order)
    10.1 --- a/src/HOL/Library/Preorder.thy	Wed Jan 10 13:35:56 2018 +0100
    10.2 +++ b/src/HOL/Library/Preorder.thy	Wed Jan 10 15:21:49 2018 +0100
    10.3 @@ -13,7 +13,7 @@
    10.4    where "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
    10.5  
    10.6  notation
    10.7 -  equiv ("op \<approx>") and
    10.8 +  equiv ("'(\<approx>')") and
    10.9    equiv ("(_/ \<approx> _)"  [51, 51] 50)
   10.10  
   10.11  lemma refl [iff]: "x \<approx> x"
    11.1 --- a/src/HOL/Orderings.thy	Wed Jan 10 13:35:56 2018 +0100
    11.2 +++ b/src/HOL/Orderings.thy	Wed Jan 10 15:21:49 2018 +0100
    11.3 @@ -132,9 +132,9 @@
    11.4  begin
    11.5  
    11.6  notation
    11.7 -  less_eq  ("op \<le>") and
    11.8 +  less_eq  ("'(\<le>')") and
    11.9    less_eq  ("(_/ \<le> _)"  [51, 51] 50) and
   11.10 -  less  ("op <") and
   11.11 +  less  ("'(<')") and
   11.12    less  ("(_/ < _)"  [51, 51] 50)
   11.13  
   11.14  abbreviation (input)
   11.15 @@ -146,7 +146,7 @@
   11.16    where "x > y \<equiv> y < x"
   11.17  
   11.18  notation (ASCII)
   11.19 -  less_eq  ("op <=") and
   11.20 +  less_eq  ("'(<=')") and
   11.21    less_eq  ("(_/ <= _)" [51, 51] 50)
   11.22  
   11.23  notation (input)
   11.24 @@ -215,7 +215,7 @@
   11.25  text \<open>Dual order\<close>
   11.26  
   11.27  lemma dual_preorder:
   11.28 -  "class.preorder (op \<ge>) (op >)"
   11.29 +  "class.preorder (\<ge>) (>)"
   11.30    by standard (auto simp add: less_le_not_le intro: order_trans)
   11.31  
   11.32  end
   11.33 @@ -348,7 +348,7 @@
   11.34  text \<open>Dual order\<close>
   11.35  
   11.36  lemma dual_order:
   11.37 -  "class.order (op \<ge>) (op >)"
   11.38 +  "class.order (\<ge>) (>)"
   11.39    using dual_order.ordering_axioms by (rule ordering_orderI)
   11.40  
   11.41  end
   11.42 @@ -430,7 +430,7 @@
   11.43  text \<open>Dual order\<close>
   11.44  
   11.45  lemma dual_linorder:
   11.46 -  "class.linorder (op \<ge>) (op >)"
   11.47 +  "class.linorder (\<ge>) (>)"
   11.48  by (rule class.linorder.intro, rule dual_order) (unfold_locales, rule linear)
   11.49  
   11.50  end
   11.51 @@ -473,7 +473,7 @@
   11.52  (* context data *)
   11.53  
   11.54  fun struct_eq ((s1: string, ts1), (s2, ts2)) =
   11.55 -  s1 = s2 andalso eq_list (op aconv) (ts1, ts2);
   11.56 +  s1 = s2 andalso eq_list (aconv) (ts1, ts2);
   11.57  
   11.58  structure Data = Generic_Data
   11.59  (
   11.60 @@ -575,83 +575,83 @@
   11.61  context order
   11.62  begin
   11.63  
   11.64 -(* The type constraint on @{term op =} below is necessary since the operation
   11.65 +(* The type constraint on @{term (=}) below is necessary since the operation
   11.66     is not a parameter of the locale. *)
   11.67  
   11.68 -declare less_irrefl [THEN notE, order add less_reflE: order "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" "op <=" "op <"]
   11.69 +declare less_irrefl [THEN notE, order add less_reflE: order "(=) :: 'a \<Rightarrow> 'a \<Rightarrow> bool" "(<=)" "(<)"]
   11.70  
   11.71 -declare order_refl  [order add le_refl: order "op = :: 'a => 'a => bool" "op <=" "op <"]
   11.72 +declare order_refl  [order add le_refl: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
   11.73  
   11.74 -declare less_imp_le [order add less_imp_le: order "op = :: 'a => 'a => bool" "op <=" "op <"]
   11.75 +declare less_imp_le [order add less_imp_le: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
   11.76  
   11.77 -declare antisym [order add eqI: order "op = :: 'a => 'a => bool" "op <=" "op <"]
   11.78 +declare antisym [order add eqI: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
   11.79  
   11.80 -declare eq_refl [order add eqD1: order "op = :: 'a => 'a => bool" "op <=" "op <"]
   11.81 +declare eq_refl [order add eqD1: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
   11.82  
   11.83 -declare sym [THEN eq_refl, order add eqD2: order "op = :: 'a => 'a => bool" "op <=" "op <"]
   11.84 +declare sym [THEN eq_refl, order add eqD2: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
   11.85  
   11.86 -declare less_trans [order add less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
   11.87 +declare less_trans [order add less_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
   11.88  
   11.89 -declare less_le_trans [order add less_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
   11.90 +declare less_le_trans [order add less_le_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
   11.91  
   11.92 -declare le_less_trans [order add le_less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
   11.93 +declare le_less_trans [order add le_less_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
   11.94  
   11.95 -declare order_trans [order add le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
   11.96 +declare order_trans [order add le_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
   11.97  
   11.98 -declare le_neq_trans [order add le_neq_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
   11.99 +declare le_neq_trans [order add le_neq_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
  11.100  
  11.101 -declare neq_le_trans [order add neq_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
  11.102 +declare neq_le_trans [order add neq_le_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
  11.103  
  11.104 -declare less_imp_neq [order add less_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"]
  11.105 +declare less_imp_neq [order add less_imp_neq: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
  11.106  
  11.107 -declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"]
  11.108 +declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
  11.109  
  11.110 -declare not_sym [order add not_sym: order "op = :: 'a => 'a => bool" "op <=" "op <"]
  11.111 +declare not_sym [order add not_sym: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
  11.112  
  11.113  end
  11.114  
  11.115  context linorder
  11.116  begin
  11.117  
  11.118 -declare [[order del: order "op = :: 'a => 'a => bool" "op <=" "op <"]]
  11.119 +declare [[order del: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]]
  11.120  
  11.121 -declare less_irrefl [THEN notE, order add less_reflE: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
  11.122 +declare less_irrefl [THEN notE, order add less_reflE: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
  11.123  
  11.124 -declare order_refl [order add le_refl: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
  11.125 +declare order_refl [order add le_refl: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
  11.126  
  11.127 -declare less_imp_le [order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
  11.128 +declare less_imp_le [order add less_imp_le: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
  11.129  
  11.130 -declare not_less [THEN iffD2, order add not_lessI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
  11.131 +declare not_less [THEN iffD2, order add not_lessI: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
  11.132  
  11.133 -declare not_le [THEN iffD2, order add not_leI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
  11.134 +declare not_le [THEN iffD2, order add not_leI: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
  11.135  
  11.136 -declare not_less [THEN iffD1, order add not_lessD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
  11.137 +declare not_less [THEN iffD1, order add not_lessD: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
  11.138  
  11.139 -declare not_le [THEN iffD1, order add not_leD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
  11.140 +declare not_le [THEN iffD1, order add not_leD: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
  11.141  
  11.142 -declare antisym [order add eqI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
  11.143 +declare antisym [order add eqI: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
  11.144  
  11.145 -declare eq_refl [order add eqD1: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
  11.146 +declare eq_refl [order add eqD1: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
  11.147  
  11.148 -declare sym [THEN eq_refl, order add eqD2: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
  11.149 +declare sym [THEN eq_refl, order add eqD2: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
  11.150  
  11.151 -declare less_trans [order add less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
  11.152 +declare less_trans [order add less_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
  11.153  
  11.154 -declare less_le_trans [order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
  11.155 +declare less_le_trans [order add less_le_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
  11.156  
  11.157 -declare le_less_trans [order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
  11.158 +declare le_less_trans [order add le_less_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
  11.159  
  11.160 -declare order_trans [order add le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
  11.161 +declare order_trans [order add le_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
  11.162  
  11.163 -declare le_neq_trans [order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
  11.164 +declare le_neq_trans [order add le_neq_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
  11.165  
  11.166 -declare neq_le_trans [order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
  11.167 +declare neq_le_trans [order add neq_le_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
  11.168  
  11.169 -declare less_imp_neq [order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
  11.170 +declare less_imp_neq [order add less_imp_neq: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
  11.171  
  11.172 -declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
  11.173 +declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
  11.174  
  11.175 -declare not_sym [order add not_sym: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
  11.176 +declare not_sym [order add not_sym: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
  11.177  
  11.178  end
  11.179  
  11.180 @@ -783,7 +783,7 @@
  11.181    fun tr' q = (q, fn _ =>
  11.182      (fn [Const (@{syntax_const "_bound"}, _) $ Free (v, T),
  11.183          Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
  11.184 -        (case AList.lookup (op =) trans (q, c, d) of
  11.185 +        (case AList.lookup (=) trans (q, c, d) of
  11.186            NONE => raise Match
  11.187          | SOME (l, g) =>
  11.188              if matches_bound v t andalso not (contains_var v u) then mk (v, T) l u P
    12.1 --- a/src/HOL/Set.thy	Wed Jan 10 13:35:56 2018 +0100
    12.2 +++ b/src/HOL/Set.thy	Wed Jan 10 15:21:49 2018 +0100
    12.3 @@ -20,19 +20,19 @@
    12.4      and Collect_mem_eq [simp]: "Collect (\<lambda>x. member x A) = A"
    12.5  
    12.6  notation
    12.7 -  member  ("op \<in>") and
    12.8 +  member  ("'(\<in>')") and
    12.9    member  ("(_/ \<in> _)" [51, 51] 50)
   12.10  
   12.11  abbreviation not_member
   12.12    where "not_member x A \<equiv> \<not> (x \<in> A)" \<comment> "non-membership"
   12.13  notation
   12.14 -  not_member  ("op \<notin>") and
   12.15 +  not_member  ("'(\<notin>')") and
   12.16    not_member  ("(_/ \<notin> _)" [51, 51] 50)
   12.17  
   12.18  notation (ASCII)
   12.19 -  member  ("op :") and
   12.20 +  member  ("'(:')") and
   12.21    member  ("(_/ : _)" [51, 51] 50) and
   12.22 -  not_member  ("op ~:") and
   12.23 +  not_member  ("'(~:')") and
   12.24    not_member  ("(_/ ~: _)" [51, 51] 50)
   12.25  
   12.26  
   12.27 @@ -155,9 +155,9 @@
   12.28    where "subset_eq \<equiv> less_eq"
   12.29  
   12.30  notation
   12.31 -  subset  ("op \<subset>") and
   12.32 +  subset  ("'(\<subset>')") and
   12.33    subset  ("(_/ \<subset> _)" [51, 51] 50) and
   12.34 -  subset_eq  ("op \<subseteq>") and
   12.35 +  subset_eq  ("'(\<subseteq>')") and
   12.36    subset_eq  ("(_/ \<subseteq> _)" [51, 51] 50)
   12.37  
   12.38  abbreviation (input)
   12.39 @@ -169,15 +169,15 @@
   12.40    "supset_eq \<equiv> greater_eq"
   12.41  
   12.42  notation
   12.43 -  supset  ("op \<supset>") and
   12.44 +  supset  ("'(\<supset>')") and
   12.45    supset  ("(_/ \<supset> _)" [51, 51] 50) and
   12.46 -  supset_eq  ("op \<supseteq>") and
   12.47 +  supset_eq  ("'(\<supseteq>')") and
   12.48    supset_eq  ("(_/ \<supseteq> _)" [51, 51] 50)
   12.49  
   12.50  notation (ASCII output)
   12.51 -  subset  ("op <") and
   12.52 +  subset  ("'(<')") and
   12.53    subset  ("(_/ < _)" [51, 51] 50) and
   12.54 -  subset_eq  ("op <=") and
   12.55 +  subset_eq  ("'(<=')") and
   12.56    subset_eq  ("(_/ <= _)" [51, 51] 50)
   12.57  
   12.58  definition Ball :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
   12.59 @@ -254,7 +254,7 @@
   12.60        (fn [Const (@{syntax_const "_bound"}, _) $ Free (v, Type (@{type_name set}, _)),
   12.61            Const (c, _) $
   12.62              (Const (d, _) $ (Const (@{syntax_const "_bound"}, _) $ Free (v', T)) $ n) $ P] =>
   12.63 -          (case AList.lookup (op =) trans (q, c, d) of
   12.64 +          (case AList.lookup (=) trans (q, c, d) of
   12.65              NONE => raise Match
   12.66            | SOME l => mk v (v', T) l n P)
   12.67          | _ => raise Match));
   12.68 @@ -305,7 +305,7 @@
   12.69          | check (Const (@{const_syntax HOL.conj}, _) $
   12.70                (Const (@{const_syntax HOL.eq}, _) $ Bound m $ e) $ P, n) =
   12.71              n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
   12.72 -            subset (op =) (0 upto (n - 1), add_loose_bnos (e, 0, []))
   12.73 +            subset (=) (0 upto (n - 1), add_loose_bnos (e, 0, []))
   12.74          | check _ = false;
   12.75  
   12.76          fun tr' (_ $ abs) =
   12.77 @@ -653,7 +653,7 @@
   12.78  subsubsection \<open>Binary intersection\<close>
   12.79  
   12.80  abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "\<inter>" 70)
   12.81 -  where "op \<inter> \<equiv> inf"
   12.82 +  where "(\<inter>) \<equiv> inf"
   12.83  
   12.84  notation (ASCII)
   12.85    inter  (infixl "Int" 70)
   12.86 @@ -957,7 +957,7 @@
   12.87  lemma bex_imageD: "\<exists>x\<in>f ` A. P x \<Longrightarrow> \<exists>x\<in>A. P (f x)"
   12.88    by auto
   12.89  
   12.90 -lemma image_add_0 [simp]: "op + (0::'a::comm_monoid_add) ` S = S"
   12.91 +lemma image_add_0 [simp]: "(+) (0::'a::comm_monoid_add) ` S = S"
   12.92    by auto
   12.93  
   12.94  
    13.1 --- a/src/Pure/Syntax/mixfix.ML	Wed Jan 10 13:35:56 2018 +0100
    13.2 +++ b/src/Pure/Syntax/mixfix.ML	Wed Jan 10 15:21:49 2018 +0100
    13.3 @@ -165,12 +165,18 @@
    13.4  val binder_stamp = stamp ();
    13.5  val binder_name = suffix "_binder";
    13.6  
    13.7 +fun mk_prefix sy =
    13.8 +  let
    13.9 +    fun star1 sys = (fst(hd sys) = "*");
   13.10 +    val sy' = Input.source_explode (Input.reset_pos sy); 
   13.11 +    val lpar = Symbol_Pos.explode0 ("'(" ^ (if star1 sy' then " " else ""));
   13.12 +    val rpar = Symbol_Pos.explode0 ((if star1(rev sy') then " " else "") ^ "')")
   13.13 + in lpar @ sy' @ rpar end
   13.14 +
   13.15  fun syn_ext_consts logical_types const_decls =
   13.16    let
   13.17      fun mk_infix sy ty c p1 p2 p3 pos =
   13.18 -      [Syntax_Ext.Mfix
   13.19 -        (Symbol_Pos.explode0 "op " @ Input.source_explode (Input.reset_pos sy),
   13.20 -          ty, c, [], 1000, Position.none),
   13.21 +      [Syntax_Ext.Mfix (mk_prefix sy, ty, c, [], 1000, Position.none),
   13.22         Syntax_Ext.Mfix
   13.23          (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)",
   13.24            ty, c, [p1, p2], p3, pos)];
    14.1 --- a/src/ZF/ex/Ring.thy	Wed Jan 10 13:35:56 2018 +0100
    14.2 +++ b/src/ZF/ex/Ring.thy	Wed Jan 10 15:21:49 2018 +0100
    14.3 @@ -46,7 +46,7 @@
    14.4    "a_inv(R) == m_inv (<carrier(R), add_field(R), zero(R), 0>)"
    14.5  
    14.6  definition
    14.7 -  minus :: "[i,i,i] => i" (infixl "\<ominus>\<index>" 65) where
    14.8 +  minus :: "[i,i,i] => i" ("(_ \<ominus>\<index> _)" [65,66] 65) where
    14.9    "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
   14.10  
   14.11  locale abelian_monoid = fixes G (structure)