--- a/NEWS Wed Jan 10 13:35:56 2018 +0100
+++ b/NEWS Wed Jan 10 15:21:49 2018 +0100
@@ -9,6 +9,15 @@
*** General ***
+* The "op <infix-op>" syntax for infix opertors has been replaced by
+"(<infix-op>)". 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".
+
* The old 'def' command has been discontinued (legacy since
Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
object-logic equality or equivalence.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/update_op Wed Jan 10 15:21:49 2018 +0100
@@ -0,0 +1,97 @@
+#!/usr/bin/env bash
+#
+# Author: Tobias Nipkow, TU Muenchen
+#
+# DESCRIPTION: update "op _" syntax
+
+## diagnostics
+
+function usage()
+{
+ echo
+ echo "Usage: isabelle $PRG [OPTIONS] [DIR]"
+ echo
+ echo " Options are:"
+ echo " -m ignore .ML files"
+ echo
+ echo " Update the old \"op _\" syntax in theory and ML files."
+ echo
+ exit 1
+}
+
+
+IGNORE_ML=""
+
+while getopts "m" OPT
+do
+ case "$OPT" in
+ m)
+ IGNORE_ML="true"
+ ;;
+ \?)
+ usage
+ ;;
+ esac
+done
+
+shift $(($OPTIND - 1))
+
+DIR="."
+if [ -n "$1" ]; then
+ DIR="$1"
+fi
+
+read -r -d '' THY_SCRIPT <<'EOF'
+# op [^]\<^bsub>*\<^esub> -> ([^]\<^bsub>*\<^esub>)
+s/\([^a-zA-Z0-9_?']\)op [ ]*\(\[\^\]\\<\^bsub>[^\\]*\\<\^esub>\)/\1(\2)/g
+# op *XY -> ( *XY)
+s/\([^a-zA-Z0-9_?']\)op[ ]*\*\([a-zA-Z][a-zA-Z]\)/\1( \*\2)/g
+# op *X -> ( *X)
+s/\([^a-zA-Z0-9_?']\)op[ ]*\*\([a-zA-Z]\)/\1( \*\2)/g
+# op *R -> ( *R)
+s/\([^a-zA-Z0-9_?']\)op[ ]*\(\*\\<^sub>[a-zA-Z]\)/\1( \2)/g
+# op *\<cdot> -> ( *\<cdot>)
+s/\([^a-zA-Z0-9_?']\)op[ ]*\(\*\\<cdot>\)/\1( \2)/g
+# op ** -> ( ** )
+s/\([^a-zA-Z0-9_?']\)op[ ]*\*\*/\1( \*\* )/g
+# op * -> ( * )
+s/\([^a-zA-Z0-9_?']\)op[ ]*\*/\1( \* )/g
+# (op +) -> (+)
+s/(op [ ]*\([^ )("][^ )(",]*\))/(\1)/g
+# (op + -> ((+)
+s/(op [ ]*\([^ )(",]*\)\([^)]\)/((\1)\2/g
+# op + -> (+)
+s/\([^a-zA-Z0-9_?']\)op [ ]*\([^ )(",:]*\)::/\1(\2)::/g
+s/\([^a-zA-Z0-9_?']\)op [ ]*\([^ )(",]*\)/\1(\2)/g
+# op+ -> (+)
+s/\([^a-zA-Z0-9_?']\)op\(\\<[a-zA-Z0-9]*>\)/\1(\2)/g
+s/\([^a-zA-Z0-9_?']\)op\([^a-zA-Z0-9_? )("\][^ )(",:]*\)::/\1(\2)::/g
+s/\([^a-zA-Z0-9_?']\)op\([^a-zA-Z0-9_? )("\][^ )(",]*\)/\1(\2)/g
+EOF
+
+read -r -d '' ML_SCRIPT <<'EOF'
+# op * -> ( * )
+s/"\(.*\)\([^a-zA-Z0-9_]\)op[ ]*\*/"\1\2( \* )/g
+s/"op[ ]*\*/"( \* )/g
+# (op +) -> (+)
+s/"\(.*\)(op [ ]*\([^ )("][^ )("]*\))/"\1(\2)/g
+s/(op [ ]*\([^ )("][^ )("]*\))\(.*\)"/(\1)\2"/g
+# (op + -> ((+)
+s/"\(.*\)(op [ ]*\([^ )("]*\)\([^)]\)/"\1((\2)\3/g
+# op + -> (+)
+s/"\(.*\)\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)/"\1\2(\3)/g
+s/"op [ ]*\([^ )("]*\)/"(\1)/g
+# op+ -> (+)
+s/"\(.*\)\([^a-zA-Z0-9_]\)op\([^a-zA-Z0-9_ )("][^ )("]*\)/"\1\2(\3)/g
+s/"op\([^a-zA-Z0-9_ )("][^ )("]*\)/"(\1)/g
+# is there \<...\> on the line (indicating Isabelle source):
+s/\\<\([^>]*\)>\(.*\)\([^a-zA-Z0-9_]\)op \*/\\<\1>\2\3( * )/g
+s/\\<\([^>]*\)>\(.*\)\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)\\<close>/\\<\1>\2\3(\4)\\<close>/g
+s/\\<\([^>]*\)>\(.*\)\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)/\\<\1>\2\3(\4)/g
+s/\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)\(.*\)\\<\([^>]*\)>/\1(\2)\3\\<\4>/g
+EOF
+
+find "$DIR" -name "*.thy" -exec sed '-i~~' -e "$THY_SCRIPT" {} \;
+
+[ "$IGNORE_ML" = "true" ] || find "$DIR" -name "*.ML" -exec sed '-i~~' -e "$ML_SCRIPT" {} \;
+
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Wed Jan 10 13:35:56 2018 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Wed Jan 10 15:21:49 2018 +0100
@@ -439,9 +439,11 @@
the delimiter is preceded by a space and followed by a space or line break;
the entire phrase is a pretty printing block.
- The alternative notation \<^verbatim>\<open>op\<close>~\<open>sy\<close> is introduced in addition. Thus any
- infix operator may be written in prefix form (as in ML), independently of
- the number of arguments in the term.
+ The alternative notation \<^verbatim>\<open>(\<close>\<open>sy\<close>\<^verbatim>\<open>)\<close> is introduced in addition. Thus any
+ infix operator may be written in prefix form (as in Haskell), independently of
+ the number of arguments in the term. To avoid conflict with the comment brackets
+ \<^verbatim>\<open>(*\<close> and \<^verbatim>\<open>*)\<close>, infix operators that begin or end with a \<^verbatim>\<open>*\<close> require
+ extra spaces, e.g. \<^verbatim>\<open>( * )\<close>.
\<close>
@@ -698,8 +700,8 @@
& \<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> \\
& \<open>|\<close> & \<^verbatim>\<open>%\<close> \<open>pttrns\<close> \<^verbatim>\<open>.\<close> \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\
& \<open>|\<close> & \<open>\<lambda>\<close> \<open>pttrns\<close> \<^verbatim>\<open>.\<close> \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\
- & \<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> \\
- & \<open>|\<close> & \<^verbatim>\<open>op\<close> \<^verbatim>\<open>==>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>op\<close> \<open>\<Longrightarrow>\<close> \\
+ & \<open>|\<close> & \<^verbatim>\<open>(==)\<close>~~\<open>|\<close>~~\<^verbatim>\<open>(\<close>\<open>\<equiv>\<close>\<^verbatim>\<open>)\<close>~~\<open>|\<close>~~\<^verbatim>\<open>(&&&)\<close> \\
+ & \<open>|\<close> & \<^verbatim>\<open>(==>)\<close>~~\<open>|\<close>~~\<^verbatim>\<open>(\<close>\<open>\<Longrightarrow>\<close>\<^verbatim>\<open>)\<close> \\
& \<open>|\<close> & \<^verbatim>\<open>TYPE\<close> \<^verbatim>\<open>(\<close> \<open>type\<close> \<^verbatim>\<open>)\<close> \\\\
@{syntax_def (inner) idt} & = & \<^verbatim>\<open>(\<close> \<open>idt\<close> \<^verbatim>\<open>)\<close>~~\<open>| id |\<close>~~\<^verbatim>\<open>_\<close> \\
--- a/src/Doc/Locales/Examples.thy Wed Jan 10 13:35:56 2018 +0100
+++ b/src/Doc/Locales/Examples.thy Wed Jan 10 15:21:49 2018 +0100
@@ -77,7 +77,7 @@
\begin{small}
\begin{alltt}
\isakeyword{fixes} le :: "'a \(\Rightarrow\) 'a \(\Rightarrow\) bool" (\isakeyword{infixl} "\(\sqsubseteq\)" 50)
- \isakeyword{assumes} "partial_order op \(\sqsubseteq\)"
+ \isakeyword{assumes} "partial_order (\(\sqsubseteq\))"
\isakeyword{notes} assumption
refl [intro, simp] = `?x \(\sqsubseteq\) ?x`
\isakeyword{and}
--- a/src/Doc/Locales/Examples3.thy Wed Jan 10 13:35:56 2018 +0100
+++ b/src/Doc/Locales/Examples3.thy Wed Jan 10 15:21:49 2018 +0100
@@ -5,9 +5,9 @@
subsection \<open>Third Version: Local Interpretation
\label{sec:local-interpretation}\<close>
-text \<open>In the above example, the fact that @{term "op \<le>"} is a partial
+text \<open>In the above example, the fact that @{term "(\<le>)"} is a partial
order for the integers was used in the second goal to
- discharge the premise in the definition of @{text "op \<sqsubset>"}. In
+ discharge the premise in the definition of @{text "(\<sqsubset>)"}. In
general, proofs of the equations not only may involve definitions
from the interpreted locale but arbitrarily complex arguments in the
context of the locale. Therefore it would be convenient to have the
@@ -16,12 +16,12 @@
The command for local interpretations is \isakeyword{interpret}. We
repeat the example from the previous section to illustrate this.\<close>
- interpretation %visible int: partial_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
+ interpretation %visible int: partial_order "(\<le>) :: int \<Rightarrow> int \<Rightarrow> bool"
rewrites "int.less x y = (x < y)"
proof -
- show "partial_order (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
+ show "partial_order ((\<le>) :: int \<Rightarrow> int \<Rightarrow> bool)"
by unfold_locales auto
- then interpret int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool" .
+ then interpret int: partial_order "(\<le>) :: [int, int] \<Rightarrow> bool" .
show "int.less x y = (x < y)"
unfolding int.less_def by auto
qed
@@ -46,11 +46,11 @@
elaborate interpretation proof. Note that the equations are named
so they can be used in a later example.\<close>
- interpretation %visible int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
+ interpretation %visible int: lattice "(\<le>) :: int \<Rightarrow> int \<Rightarrow> bool"
rewrites int_min_eq: "int.meet x y = min x y"
and int_max_eq: "int.join x y = max x y"
proof -
- show "lattice (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
+ show "lattice ((\<le>) :: int \<Rightarrow> int \<Rightarrow> bool)"
txt \<open>\normalsize We have already shown that this is a partial
order,\<close>
apply unfold_locales
@@ -68,17 +68,17 @@
txt \<open>\normalsize In order to show the equations, we put ourselves
in a situation where the lattice theorems can be used in a
convenient way.\<close>
- then interpret int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" .
+ then interpret int: lattice "(\<le>) :: int \<Rightarrow> int \<Rightarrow> bool" .
show "int.meet x y = min x y"
by (bestsimp simp: int.meet_def int.is_inf_def)
show "int.join x y = max x y"
by (bestsimp simp: int.join_def int.is_sup_def)
qed
-text \<open>Next follows that @{text "op \<le>"} is a total order, again for
+text \<open>Next follows that @{text "(\<le>)"} is a total order, again for
the integers.\<close>
- interpretation %visible int: total_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
+ interpretation %visible int: total_order "(\<le>) :: int \<Rightarrow> int \<Rightarrow> bool"
by unfold_locales arith
text \<open>Theorems that are available in the theory at this point are shown in
@@ -115,9 +115,9 @@
the \isakeyword{sublocale} command. Existing interpretations are
skipped avoiding duplicate work.
\item
- The predicate @{term "op <"} appears in theorem @{thm [source]
+ The predicate @{term "(<)"} appears in theorem @{thm [source]
int.less_total}
- although an equation for the replacement of @{text "op \<sqsubset>"} was only
+ although an equation for the replacement of @{text "(\<sqsubset>)"} was only
given in the interpretation of @{text partial_order}. The
interpretation equations are pushed downwards the hierarchy for
related interpretations --- that is, for interpretations that share
@@ -132,7 +132,7 @@
outputs the following:
\begin{small}
\begin{alltt}
- int : partial_order "op \(\le\)"
+ int : partial_order "(\(\le\))"
\end{alltt}
\end{small}
Of course, there is only one interpretation.
@@ -220,8 +220,8 @@
\hspace*{1em}@{thm [source] le'.less_le_trans}:
@{thm [display, indent=4] le'.less_le_trans}
While there is infix syntax for the strict operation associated with
- @{term "op \<sqsubseteq>"}, there is none for the strict version of @{term
- "op \<preceq>"}. The syntax @{text "\<sqsubset>"} for @{text less} is only
+ @{term "(\<sqsubseteq>)"}, there is none for the strict version of @{term
+ "(\<preceq>)"}. The syntax @{text "\<sqsubset>"} for @{text less} is only
available for the original instance it was declared for. We may
introduce infix syntax for @{text le'.less} with the following declaration:\<close>
@@ -390,7 +390,7 @@
certain conditions are fulfilled. Take, for example, the function
@{text "\<lambda>i. n * i"} that scales its argument by a constant factor.
This function is order preserving (and even a lattice endomorphism)
- with respect to @{term "op \<le>"} provided @{text "n \<ge> 0"}.
+ with respect to @{term "(\<le>)"} provided @{text "n \<ge> 0"}.
It is not possible to express this using a global interpretation,
because it is in general unspecified whether~@{term n} is
@@ -412,14 +412,14 @@
lattice endomorphisms.\<close>
sublocale non_negative \<subseteq>
- order_preserving "op \<le>" "op \<le>" "\<lambda>i. n * i"
+ order_preserving "(\<le>)" "(\<le>)" "\<lambda>i. n * i"
using non_neg by unfold_locales (rule mult_left_mono)
text \<open>While the proof of the previous interpretation
- is straightforward from monotonicity lemmas for~@{term "op *"}, the
+ is straightforward from monotonicity lemmas for~@{term "( * )"}, the
second proof follows a useful pattern.\<close>
- sublocale %visible non_negative \<subseteq> lattice_end "op \<le>" "\<lambda>i. n * i"
+ sublocale %visible non_negative \<subseteq> lattice_end "(\<le>)" "\<lambda>i. n * i"
proof (unfold_locales, unfold int_min_eq int_max_eq)
txt \<open>\normalsize Unfolding the locale predicates \emph{and} the
interpretation equations immediately yields two subgoals that
--- a/src/Doc/Tutorial/Documents/Documents.thy Wed Jan 10 13:35:56 2018 +0100
+++ b/src/Doc/Tutorial/Documents/Documents.thy Wed Jan 10 15:21:49 2018 +0100
@@ -44,10 +44,10 @@
\noindent Now @{text "xor A B"} and @{text "A [+] B"} refer to the
same expression internally. Any curried function with at least two
arguments may be given infix syntax. For partial applications with
- fewer than two operands, there is a notation using the prefix~@{text
- op}. For instance, @{text xor} without arguments is represented as
- @{text "op [+]"}; together with ordinary function application, this
- turns @{text "xor A"} into @{text "op [+] A"}.
+ fewer than two operands, the operator is enclosed in parentheses.
+ For instance, @{text xor} without arguments is represented as
+ @{text "([+])"}; together with ordinary function application, this
+ turns @{text "xor A"} into @{text "([+]) A"}.
The keyword \isakeyword{infixl} seen above specifies an
infix operator that is nested to the \emph{left}: in iterated
--- a/src/HOL/Algebra/Ring.thy Wed Jan 10 13:35:56 2018 +0100
+++ b/src/HOL/Algebra/Ring.thy Wed Jan 10 15:21:49 2018 +0100
@@ -22,7 +22,7 @@
where "a_inv R = m_inv \<lparr>carrier = carrier R, mult = add R, one = zero R\<rparr>"
definition
- a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
+ a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" ("(_ \<ominus>\<index> _)" [65,66] 65)
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)"
locale abelian_monoid =
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Jan 10 13:35:56 2018 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Jan 10 15:21:49 2018 +0100
@@ -394,12 +394,12 @@
lemmas dlo_simps[no_atp] = order_refl less_irrefl not_less not_le exists_neq
le_less neq_iff linear less_not_permute
-lemma axiom[no_atp]: "class.unbounded_dense_linorder (op \<le>) (op <)"
+lemma axiom[no_atp]: "class.unbounded_dense_linorder (\<le>) (<)"
by (rule unbounded_dense_linorder_axioms)
lemma atoms[no_atp]:
shows "TERM (less :: 'a \<Rightarrow> _)"
and "TERM (less_eq :: 'a \<Rightarrow> _)"
- and "TERM (op = :: 'a \<Rightarrow> _)" .
+ and "TERM ((=) :: 'a \<Rightarrow> _)" .
declare axiom[langford qe: dlo_qe_bnds dlo_qe_nolb dlo_qe_noub gather: gather_start gather_simps atoms: atoms]
declare dlo_simps[langfordsimp]
@@ -438,9 +438,9 @@
begin
notation
- less_eq ("op \<sqsubseteq>") and
+ less_eq ("'(\<sqsubseteq>')") and
less_eq ("(_/ \<sqsubseteq> _)" [51, 51] 50) and
- less ("op \<sqsubset>") and
+ less ("'(\<sqsubset>')") and
less ("(_/ \<sqsubset> _)" [51, 51] 50)
end
@@ -705,7 +705,7 @@
lemma atoms[no_atp]:
shows "TERM (less :: 'a \<Rightarrow> _)"
and "TERM (less_eq :: 'a \<Rightarrow> _)"
- and "TERM (op = :: 'a \<Rightarrow> _)" .
+ and "TERM ((=) :: 'a \<Rightarrow> _)" .
declare ferrack_axiom [ferrack minf: minf_thms pinf: pinf_thms
nmi: nmi_thms npi: npi_thms lindense:
@@ -716,7 +716,7 @@
fun simps phi = map (Morphism.thm phi) [@{thm "not_less"}, @{thm "not_le"}]
fun generic_whatis phi =
let
- val [lt, le] = map (Morphism.term phi) [@{term "op \<sqsubset>"}, @{term "op \<sqsubseteq>"}]
+ val [lt, le] = map (Morphism.term phi) [@{term "(\<sqsubset>)"}, @{term "(\<sqsubseteq>)"}]
fun h x t =
case Thm.term_of t of
Const(@{const_name HOL.eq}, _)$y$z =>
@@ -885,7 +885,7 @@
using eq_diff_eq[where a= x and b=t and c=0] by simp
interpretation class_dense_linordered_field: constr_dense_linorder
- "op \<le>" "op <" "\<lambda>x y. 1/2 * ((x::'a::linordered_field) + y)"
+ "(\<le>)" "(<)" "\<lambda>x y. 1/2 * ((x::'a::linordered_field) + y)"
by unfold_locales (dlo, dlo, auto)
declaration \<open>
--- a/src/HOL/Library/Multiset.thy Wed Jan 10 13:35:56 2018 +0100
+++ b/src/HOL/Library/Multiset.thy Wed Jan 10 15:21:49 2018 +0100
@@ -148,22 +148,22 @@
where "Melem a M \<equiv> a \<in> set_mset M"
notation
- Melem ("op \<in>#") and
+ Melem ("'(\<in>#')") and
Melem ("(_/ \<in># _)" [51, 51] 50)
notation (ASCII)
- Melem ("op :#") and
+ Melem ("'(:#')") and
Melem ("(_/ :# _)" [51, 51] 50)
abbreviation not_Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"
where "not_Melem a M \<equiv> a \<notin> set_mset M"
notation
- not_Melem ("op \<notin>#") and
+ not_Melem ("'(\<notin>#')") and
not_Melem ("(_/ \<notin># _)" [51, 51] 50)
notation (ASCII)
- not_Melem ("op ~:#") and
+ not_Melem ("'(~:#')") and
not_Melem ("(_/ ~:# _)" [51, 51] 50)
context
@@ -533,11 +533,11 @@
supseteq_mset (infix ">=#" 50) and
supset_mset (infix ">#" 50)
-interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op -" "op \<subseteq>#" "op \<subset>#"
+interpretation subset_mset: ordered_ab_semigroup_add_imp_le "(+)" "(-)" "(\<subseteq>#)" "(\<subset>#)"
by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
\<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
-interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "op +" 0 "op -" "op \<subseteq>#" "op \<subset>#"
+interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "(+)" 0 "(-)" "(\<subseteq>#)" "(\<subset>#)"
by standard
\<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
@@ -556,7 +556,7 @@
apply (auto intro: multiset_eq_iff [THEN iffD2])
done
-interpretation subset_mset: ordered_cancel_comm_monoid_diff "op +" 0 "op \<subseteq>#" "op \<subset>#" "op -"
+interpretation subset_mset: ordered_cancel_comm_monoid_diff "(+)" 0 "(\<subseteq>#)" "(\<subset>#)" "(-)"
by standard (simp, fact mset_subset_eq_exists_conv)
\<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
@@ -690,27 +690,27 @@
definition inf_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "\<inter>#" 70) where
multiset_inter_def: "inf_subset_mset A B = A - (A - B)"
-interpretation subset_mset: semilattice_inf inf_subset_mset "op \<subseteq>#" "op \<subset>#"
+interpretation subset_mset: semilattice_inf inf_subset_mset "(\<subseteq>#)" "(\<subset>#)"
proof -
have [simp]: "m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" for m n q :: nat
by arith
- show "class.semilattice_inf op \<inter># op \<subseteq># op \<subset>#"
+ show "class.semilattice_inf (\<inter>#) (\<subseteq>#) (\<subset>#)"
by standard (auto simp add: multiset_inter_def subseteq_mset_def)
qed \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
definition sup_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"(infixl "\<union>#" 70)
where "sup_subset_mset A B = A + (B - A)" \<comment> \<open>FIXME irregular fact name\<close>
-interpretation subset_mset: semilattice_sup sup_subset_mset "op \<subseteq>#" "op \<subset>#"
+interpretation subset_mset: semilattice_sup sup_subset_mset "(\<subseteq>#)" "(\<subset>#)"
proof -
have [simp]: "m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q - m) \<le> n" for m n q :: nat
by arith
- show "class.semilattice_sup op \<union># op \<subseteq># op \<subset>#"
+ show "class.semilattice_sup (\<union>#) (\<subseteq>#) (\<subset>#)"
by standard (auto simp add: sup_subset_mset_def subseteq_mset_def)
qed \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
-interpretation subset_mset: bounded_lattice_bot "op \<inter>#" "op \<subseteq>#" "op \<subset>#"
- "op \<union>#" "{#}"
+interpretation subset_mset: bounded_lattice_bot "(\<inter>#)" "(\<subseteq>#)" "(\<subset>#)"
+ "(\<union>#)" "{#}"
by standard auto
\<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
@@ -1120,7 +1120,7 @@
using assms by (simp add: Sup_multiset_def Abs_multiset_inverse Sup_multiset_in_multiset)
-interpretation subset_mset: conditionally_complete_lattice Inf Sup "op \<inter>#" "op \<subseteq>#" "op \<subset>#" "op \<union>#"
+interpretation subset_mset: conditionally_complete_lattice Inf Sup "(\<inter>#)" "(\<subseteq>#)" "(\<subset>#)" "(\<union>#)"
proof
fix X :: "'a multiset" and A
assume "X \<in> A"
@@ -1244,7 +1244,7 @@
with assms show ?thesis by (simp add: in_Sup_multiset_iff)
qed
-interpretation subset_mset: distrib_lattice "op \<inter>#" "op \<subseteq>#" "op \<subset>#" "op \<union>#"
+interpretation subset_mset: distrib_lattice "(\<inter>#)" "(\<subseteq>#)" "(\<subset>#)" "(\<union>#)"
proof
fix A B C :: "'a multiset"
show "A \<union># (B \<inter># C) = A \<union># B \<inter># (A \<union># C)"
@@ -2269,12 +2269,12 @@
end
end
-lemma comp_fun_commute_plus_mset[simp]: "comp_fun_commute (op + :: 'a multiset \<Rightarrow> _ \<Rightarrow> _)"
+lemma comp_fun_commute_plus_mset[simp]: "comp_fun_commute ((+) :: 'a multiset \<Rightarrow> _ \<Rightarrow> _)"
by standard (simp add: add_ac comp_def)
declare comp_fun_commute.fold_mset_add_mset[OF comp_fun_commute_plus_mset, simp]
-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)"
+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)"
by (induct NN) auto
context comm_monoid_add
@@ -2626,7 +2626,7 @@
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
then have "\<And>P. [x \<leftarrow> sort_key f xs . P (f x) ?pivot \<and> f l = f x] =
[x \<leftarrow> sort_key f xs. P (f l) ?pivot \<and> f l = f x]" by simp
- note *** = this [of "op <"] this [of "op >"] this [of "op ="]
+ note *** = this [of "(<)"] this [of "(>)"] this [of "(=)"]
show "[x \<leftarrow> ?rhs. f l = f x] = [x \<leftarrow> ?lhs. f l = f x]"
proof (cases "f l" ?pivot rule: linorder_cases)
case less
@@ -2998,7 +2998,7 @@
text \<open>
Predicate variants of \<open>mult\<close> and the reflexive closure of \<open>mult\<close>, which are
executable whenever the given predicate \<open>P\<close> is. Together with the standard
- code equations for \<open>op \<inter>#\<close> and \<open>op -\<close> this should yield quadratic
+ code equations for \<open>(\<inter>#\<close>) and \<open>(-\<close>) this should yield quadratic
(with respect to calls to \<open>P\<close>) implementations of \<open>multp\<close> and \<open>multeqp\<close>.
\<close>
@@ -3346,10 +3346,10 @@
let
val (maybe_opt, ps) =
Nitpick_Model.dest_plain_fun t'
- ||> op ~~
+ ||> (~~)
||> map (apsnd (snd o HOLogic.dest_number))
fun elems_for t =
- (case AList.lookup (op =) ps t of
+ (case AList.lookup (=) ps t of
SOME n => replicate n t
| NONE => [Const (maybe_name, elem_T --> elem_T) $ t])
in
@@ -3438,7 +3438,7 @@
fun subset_eq_mset_impl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool option" where
"subset_eq_mset_impl [] ys = Some (ys \<noteq> [])"
-| "subset_eq_mset_impl (Cons x xs) ys = (case List.extract (op = x) ys of
+| "subset_eq_mset_impl (Cons x xs) ys = (case List.extract ((=) x) ys of
None \<Rightarrow> None
| Some (ys1,_,ys2) \<Rightarrow> subset_eq_mset_impl xs (ys1 @ ys2))"
@@ -3451,7 +3451,7 @@
next
case (Cons x xs ys)
show ?case
- proof (cases "List.extract (op = x) ys")
+ proof (cases "List.extract ((=) x) ys")
case None
hence x: "x \<notin> set ys" by (simp add: extract_None_iff)
{
@@ -3510,8 +3510,8 @@
qed
text \<open>
- Exercise for the casual reader: add implementations for @{term "op \<le>"}
- and @{term "op <"} (multiset order).
+ Exercise for the casual reader: add implementations for @{term "(\<le>)"}
+ and @{term "(<)"} (multiset order).
\<close>
text \<open>Quickcheck generators\<close>
@@ -3668,7 +3668,7 @@
unfolding comp_def by (rule ext) (simp add: comp_def image_mset.compositionality)
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
by (induct X) simp_all
- show "set_mset \<circ> image_mset f = op ` f \<circ> set_mset" for f
+ show "set_mset \<circ> image_mset f = (`) f \<circ> set_mset" for f
by auto
show "card_order natLeq"
by (rule natLeq_card_order)
--- a/src/HOL/Library/Preorder.thy Wed Jan 10 13:35:56 2018 +0100
+++ b/src/HOL/Library/Preorder.thy Wed Jan 10 15:21:49 2018 +0100
@@ -13,7 +13,7 @@
where "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
notation
- equiv ("op \<approx>") and
+ equiv ("'(\<approx>')") and
equiv ("(_/ \<approx> _)" [51, 51] 50)
lemma refl [iff]: "x \<approx> x"
--- a/src/HOL/Orderings.thy Wed Jan 10 13:35:56 2018 +0100
+++ b/src/HOL/Orderings.thy Wed Jan 10 15:21:49 2018 +0100
@@ -132,9 +132,9 @@
begin
notation
- less_eq ("op \<le>") and
+ less_eq ("'(\<le>')") and
less_eq ("(_/ \<le> _)" [51, 51] 50) and
- less ("op <") and
+ less ("'(<')") and
less ("(_/ < _)" [51, 51] 50)
abbreviation (input)
@@ -146,7 +146,7 @@
where "x > y \<equiv> y < x"
notation (ASCII)
- less_eq ("op <=") and
+ less_eq ("'(<=')") and
less_eq ("(_/ <= _)" [51, 51] 50)
notation (input)
@@ -215,7 +215,7 @@
text \<open>Dual order\<close>
lemma dual_preorder:
- "class.preorder (op \<ge>) (op >)"
+ "class.preorder (\<ge>) (>)"
by standard (auto simp add: less_le_not_le intro: order_trans)
end
@@ -348,7 +348,7 @@
text \<open>Dual order\<close>
lemma dual_order:
- "class.order (op \<ge>) (op >)"
+ "class.order (\<ge>) (>)"
using dual_order.ordering_axioms by (rule ordering_orderI)
end
@@ -430,7 +430,7 @@
text \<open>Dual order\<close>
lemma dual_linorder:
- "class.linorder (op \<ge>) (op >)"
+ "class.linorder (\<ge>) (>)"
by (rule class.linorder.intro, rule dual_order) (unfold_locales, rule linear)
end
@@ -473,7 +473,7 @@
(* context data *)
fun struct_eq ((s1: string, ts1), (s2, ts2)) =
- s1 = s2 andalso eq_list (op aconv) (ts1, ts2);
+ s1 = s2 andalso eq_list (aconv) (ts1, ts2);
structure Data = Generic_Data
(
@@ -575,83 +575,83 @@
context order
begin
-(* The type constraint on @{term op =} below is necessary since the operation
+(* The type constraint on @{term (=}) below is necessary since the operation
is not a parameter of the locale. *)
-declare less_irrefl [THEN notE, order add less_reflE: order "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" "op <=" "op <"]
+declare less_irrefl [THEN notE, order add less_reflE: order "(=) :: 'a \<Rightarrow> 'a \<Rightarrow> bool" "(<=)" "(<)"]
-declare order_refl [order add le_refl: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare order_refl [order add le_refl: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare less_imp_le [order add less_imp_le: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare less_imp_le [order add less_imp_le: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare antisym [order add eqI: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare antisym [order add eqI: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare eq_refl [order add eqD1: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare eq_refl [order add eqD1: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare sym [THEN eq_refl, order add eqD2: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare sym [THEN eq_refl, order add eqD2: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare less_trans [order add less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare less_trans [order add less_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare less_le_trans [order add less_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare less_le_trans [order add less_le_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare le_less_trans [order add le_less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare le_less_trans [order add le_less_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare order_trans [order add le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare order_trans [order add le_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare le_neq_trans [order add le_neq_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare le_neq_trans [order add le_neq_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare neq_le_trans [order add neq_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare neq_le_trans [order add neq_le_trans: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare less_imp_neq [order add less_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare less_imp_neq [order add less_imp_neq: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare not_sym [order add not_sym: order "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare not_sym [order add not_sym: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
end
context linorder
begin
-declare [[order del: order "op = :: 'a => 'a => bool" "op <=" "op <"]]
+declare [[order del: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]]
-declare less_irrefl [THEN notE, order add less_reflE: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare less_irrefl [THEN notE, order add less_reflE: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare order_refl [order add le_refl: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare order_refl [order add le_refl: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare less_imp_le [order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare less_imp_le [order add less_imp_le: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare not_less [THEN iffD2, order add not_lessI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare not_less [THEN iffD2, order add not_lessI: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare not_le [THEN iffD2, order add not_leI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare not_le [THEN iffD2, order add not_leI: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare not_less [THEN iffD1, order add not_lessD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare not_less [THEN iffD1, order add not_lessD: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare not_le [THEN iffD1, order add not_leD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare not_le [THEN iffD1, order add not_leD: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare antisym [order add eqI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare antisym [order add eqI: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare eq_refl [order add eqD1: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare eq_refl [order add eqD1: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare sym [THEN eq_refl, order add eqD2: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare sym [THEN eq_refl, order add eqD2: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare less_trans [order add less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare less_trans [order add less_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare less_le_trans [order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare less_le_trans [order add less_le_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare le_less_trans [order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare le_less_trans [order add le_less_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare order_trans [order add le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare order_trans [order add le_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare le_neq_trans [order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare le_neq_trans [order add le_neq_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare neq_le_trans [order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare neq_le_trans [order add neq_le_trans: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare less_imp_neq [order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare less_imp_neq [order add less_imp_neq: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
-declare not_sym [order add not_sym: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
+declare not_sym [order add not_sym: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
end
@@ -783,7 +783,7 @@
fun tr' q = (q, fn _ =>
(fn [Const (@{syntax_const "_bound"}, _) $ Free (v, T),
Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
- (case AList.lookup (op =) trans (q, c, d) of
+ (case AList.lookup (=) trans (q, c, d) of
NONE => raise Match
| SOME (l, g) =>
if matches_bound v t andalso not (contains_var v u) then mk (v, T) l u P
--- a/src/HOL/Set.thy Wed Jan 10 13:35:56 2018 +0100
+++ b/src/HOL/Set.thy Wed Jan 10 15:21:49 2018 +0100
@@ -20,19 +20,19 @@
and Collect_mem_eq [simp]: "Collect (\<lambda>x. member x A) = A"
notation
- member ("op \<in>") and
+ member ("'(\<in>')") and
member ("(_/ \<in> _)" [51, 51] 50)
abbreviation not_member
where "not_member x A \<equiv> \<not> (x \<in> A)" \<comment> "non-membership"
notation
- not_member ("op \<notin>") and
+ not_member ("'(\<notin>')") and
not_member ("(_/ \<notin> _)" [51, 51] 50)
notation (ASCII)
- member ("op :") and
+ member ("'(:')") and
member ("(_/ : _)" [51, 51] 50) and
- not_member ("op ~:") and
+ not_member ("'(~:')") and
not_member ("(_/ ~: _)" [51, 51] 50)
@@ -155,9 +155,9 @@
where "subset_eq \<equiv> less_eq"
notation
- subset ("op \<subset>") and
+ subset ("'(\<subset>')") and
subset ("(_/ \<subset> _)" [51, 51] 50) and
- subset_eq ("op \<subseteq>") and
+ subset_eq ("'(\<subseteq>')") and
subset_eq ("(_/ \<subseteq> _)" [51, 51] 50)
abbreviation (input)
@@ -169,15 +169,15 @@
"supset_eq \<equiv> greater_eq"
notation
- supset ("op \<supset>") and
+ supset ("'(\<supset>')") and
supset ("(_/ \<supset> _)" [51, 51] 50) and
- supset_eq ("op \<supseteq>") and
+ supset_eq ("'(\<supseteq>')") and
supset_eq ("(_/ \<supseteq> _)" [51, 51] 50)
notation (ASCII output)
- subset ("op <") and
+ subset ("'(<')") and
subset ("(_/ < _)" [51, 51] 50) and
- subset_eq ("op <=") and
+ subset_eq ("'(<=')") and
subset_eq ("(_/ <= _)" [51, 51] 50)
definition Ball :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
@@ -254,7 +254,7 @@
(fn [Const (@{syntax_const "_bound"}, _) $ Free (v, Type (@{type_name set}, _)),
Const (c, _) $
(Const (d, _) $ (Const (@{syntax_const "_bound"}, _) $ Free (v', T)) $ n) $ P] =>
- (case AList.lookup (op =) trans (q, c, d) of
+ (case AList.lookup (=) trans (q, c, d) of
NONE => raise Match
| SOME l => mk v (v', T) l n P)
| _ => raise Match));
@@ -305,7 +305,7 @@
| check (Const (@{const_syntax HOL.conj}, _) $
(Const (@{const_syntax HOL.eq}, _) $ Bound m $ e) $ P, n) =
n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
- subset (op =) (0 upto (n - 1), add_loose_bnos (e, 0, []))
+ subset (=) (0 upto (n - 1), add_loose_bnos (e, 0, []))
| check _ = false;
fun tr' (_ $ abs) =
@@ -653,7 +653,7 @@
subsubsection \<open>Binary intersection\<close>
abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "\<inter>" 70)
- where "op \<inter> \<equiv> inf"
+ where "(\<inter>) \<equiv> inf"
notation (ASCII)
inter (infixl "Int" 70)
@@ -957,7 +957,7 @@
lemma bex_imageD: "\<exists>x\<in>f ` A. P x \<Longrightarrow> \<exists>x\<in>A. P (f x)"
by auto
-lemma image_add_0 [simp]: "op + (0::'a::comm_monoid_add) ` S = S"
+lemma image_add_0 [simp]: "(+) (0::'a::comm_monoid_add) ` S = S"
by auto
--- a/src/Pure/Syntax/mixfix.ML Wed Jan 10 13:35:56 2018 +0100
+++ b/src/Pure/Syntax/mixfix.ML Wed Jan 10 15:21:49 2018 +0100
@@ -165,12 +165,18 @@
val binder_stamp = stamp ();
val binder_name = suffix "_binder";
+fun mk_prefix sy =
+ let
+ fun star1 sys = (fst(hd sys) = "*");
+ val sy' = Input.source_explode (Input.reset_pos sy);
+ val lpar = Symbol_Pos.explode0 ("'(" ^ (if star1 sy' then " " else ""));
+ val rpar = Symbol_Pos.explode0 ((if star1(rev sy') then " " else "") ^ "')")
+ in lpar @ sy' @ rpar end
+
fun syn_ext_consts logical_types const_decls =
let
fun mk_infix sy ty c p1 p2 p3 pos =
- [Syntax_Ext.Mfix
- (Symbol_Pos.explode0 "op " @ Input.source_explode (Input.reset_pos sy),
- ty, c, [], 1000, Position.none),
+ [Syntax_Ext.Mfix (mk_prefix sy, ty, c, [], 1000, Position.none),
Syntax_Ext.Mfix
(Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)",
ty, c, [p1, p2], p3, pos)];
--- a/src/ZF/ex/Ring.thy Wed Jan 10 13:35:56 2018 +0100
+++ b/src/ZF/ex/Ring.thy Wed Jan 10 15:21:49 2018 +0100
@@ -46,7 +46,7 @@
"a_inv(R) == m_inv (<carrier(R), add_field(R), zero(R), 0>)"
definition
- minus :: "[i,i,i] => i" (infixl "\<ominus>\<index>" 65) where
+ minus :: "[i,i,i] => i" ("(_ \<ominus>\<index> _)" [65,66] 65) where
"\<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)"
locale abelian_monoid = fixes G (structure)