--- a/src/Doc/Tutorial/CTL/CTL.thy Fri Sep 27 22:44:30 2024 +0200
+++ b/src/Doc/Tutorial/CTL/CTL.thy Fri Sep 27 23:47:45 2024 +0200
@@ -35,7 +35,7 @@
a new datatype and a new function.}
\<close>
(*<*)
-primrec valid :: "state \<Rightarrow> formula \<Rightarrow> bool" (\<open>(_ \<Turnstile> _)\<close> [80,80] 80) where
+primrec valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80) where
"s \<Turnstile> Atom a = (a \<in> L s)" |
"s \<Turnstile> Neg f = (~(s \<Turnstile> f))" |
"s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)" |
--- a/src/Doc/Tutorial/CTL/PDL.thy Fri Sep 27 22:44:30 2024 +0200
+++ b/src/Doc/Tutorial/CTL/PDL.thy Fri Sep 27 23:47:45 2024 +0200
@@ -26,7 +26,7 @@
\hbox{\<open>valid s f\<close>}. The definition is by recursion over the syntax:
\<close>
-primrec valid :: "state \<Rightarrow> formula \<Rightarrow> bool" (\<open>(_ \<Turnstile> _)\<close> [80,80] 80)
+primrec valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80)
where
"s \<Turnstile> Atom a = (a \<in> L s)" |
"s \<Turnstile> Neg f = (\<not>(s \<Turnstile> f))" |
--- a/src/Doc/Tutorial/Documents/Documents.thy Fri Sep 27 22:44:30 2024 +0200
+++ b/src/Doc/Tutorial/Documents/Documents.thy Fri Sep 27 23:47:45 2024 +0200
@@ -37,7 +37,7 @@
operation on boolean values illustrates typical infix declarations.
\<close>
-definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl \<open>[+]\<close> 60)
+definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "[+]" 60)
where "A [+] B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
text \<open>
@@ -138,7 +138,7 @@
hide_const xor
setup \<open>Sign.add_path "version1"\<close>
(*>*)
-definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl \<open>\<oplus>\<close> 60)
+definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "\<oplus>" 60)
where "A \<oplus> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
(*<*)
setup \<open>Sign.local_path\<close>
@@ -156,10 +156,10 @@
hide_const xor
setup \<open>Sign.add_path "version2"\<close>
(*>*)
-definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl \<open>[+]\<ignore>\<close> 60)
+definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "[+]\<ignore>" 60)
where "A [+]\<ignore> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
-notation (xsymbols) xor (infixl \<open>\<oplus>\<ignore>\<close> 60)
+notation (xsymbols) xor (infixl "\<oplus>\<ignore>" 60)
(*<*)
setup \<open>Sign.local_path\<close>
(*>*)
@@ -186,10 +186,10 @@
\<close>
datatype currency =
- Euro nat (\<open>\<euro>\<close>)
- | Pounds nat (\<open>\<pounds>\<close>)
- | Yen nat (\<open>\<yen>\<close>)
- | Dollar nat (\<open>$\<close>)
+ Euro nat ("\<euro>")
+ | Pounds nat ("\<pounds>")
+ | Yen nat ("\<yen>")
+ | Dollar nat ("$")
text \<open>
\noindent Here the mixfix annotations on the rightmost column happen
@@ -223,7 +223,7 @@
\<open>x \<approx> y\<close>. We assume that a constant \<open>sim\<close> of type
\<^typ>\<open>('a \<times> 'a) set\<close> has been introduced at this point.\<close>
(*<*)consts sim :: "('a \<times> 'a) set"(*>*)
-abbreviation sim2 :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix \<open>\<approx>\<close> 50)
+abbreviation sim2 :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<approx>" 50)
where "x \<approx> y \<equiv> (x, y) \<in> sim"
text \<open>\noindent The given meta-equality is used as a rewrite rule
@@ -238,10 +238,10 @@
stems from Isabelle/HOL itself:
\<close>
-abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl \<open>~=\<ignore>\<close> 50)
+abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "~=\<ignore>" 50)
where "x ~=\<ignore> y \<equiv> \<not> (x = y)"
-notation (xsymbols) not_equal (infix \<open>\<noteq>\<ignore>\<close> 50)
+notation (xsymbols) not_equal (infix "\<noteq>\<ignore>" 50)
text \<open>\noindent The notation \<open>\<noteq>\<close> is introduced separately to restrict it
to the \emph{xsymbols} mode.
--- a/src/Doc/Tutorial/Inductive/Star.thy Fri Sep 27 22:44:30 2024 +0200
+++ b/src/Doc/Tutorial/Inductive/Star.thy Fri Sep 27 23:47:45 2024 +0200
@@ -15,7 +15,7 @@
\<close>
inductive_set
- rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" (\<open>_*\<close> [1000] 999)
+ rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" ("_*" [1000] 999)
for r :: "('a \<times> 'a)set"
where
rtc_refl[iff]: "(x,x) \<in> r*"
--- a/src/Doc/Tutorial/Misc/fakenat.thy Fri Sep 27 22:44:30 2024 +0200
+++ b/src/Doc/Tutorial/Misc/fakenat.thy Fri Sep 27 23:47:45 2024 +0200
@@ -8,7 +8,7 @@
It behaves approximately as if it were declared like this:
\<close>
-datatype nat = zero (\<open>0\<close>) | Suc nat
+datatype nat = zero ("0") | Suc nat
(*<*)
end
(*>*)
--- a/src/Doc/Tutorial/Protocol/Message.thy Fri Sep 27 22:44:30 2024 +0200
+++ b/src/Doc/Tutorial/Protocol/Message.thy Fri Sep 27 23:47:45 2024 +0200
@@ -81,9 +81,9 @@
text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
nonterminal mtuple_args
syntax
- "" :: "'a \<Rightarrow> mtuple_args" (\<open>_\<close>)
- "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args" (\<open>_,/ _\<close>)
- "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b" (\<open>(2\<lbrace>_,/ _\<rbrace>)\<close>)
+ "" :: "'a \<Rightarrow> mtuple_args" ("_")
+ "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args" ("_,/ _")
+ "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
syntax_consts
"_MTuple_args" "_MTuple" \<rightleftharpoons> MPair
translations
--- a/src/Doc/Tutorial/ToyList/ToyList.thy Fri Sep 27 22:44:30 2024 +0200
+++ b/src/Doc/Tutorial/ToyList/ToyList.thy Fri Sep 27 23:47:45 2024 +0200
@@ -9,12 +9,12 @@
the concrete syntax and name space of theory \<^theory>\<open>Main\<close> as follows.
\<close>
-no_notation Nil (\<open>[]\<close>) and Cons (infixr \<open>#\<close> 65) and append (infixr \<open>@\<close> 65)
+no_notation Nil ("[]") and Cons (infixr "#" 65) and append (infixr "@" 65)
hide_type list
hide_const rev
-datatype 'a list = Nil (\<open>[]\<close>)
- | Cons 'a "'a list" (infixr \<open>#\<close> 65)
+datatype 'a list = Nil ("[]")
+ | Cons 'a "'a list" (infixr "#" 65)
text\<open>\noindent
The datatype\index{datatype@\isacommand {datatype} (command)}
@@ -47,7 +47,7 @@
in this order, because Isabelle insists on definition before use:
\<close>
-primrec app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr \<open>@\<close> 65) where
+primrec app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) where
"[] @ ys = ys" |
"(x # xs) @ ys = x # (xs @ ys)"
--- a/src/Doc/Tutorial/Types/Axioms.thy Fri Sep 27 22:44:30 2024 +0200
+++ b/src/Doc/Tutorial/Types/Axioms.thy Fri Sep 27 23:47:45 2024 +0200
@@ -84,7 +84,7 @@
parameter \<open>neutral\<close> together with its property:\<close>
class monoidl = semigroup +
- fixes neutral :: "'a" (\<open>\<zero>\<close>)
+ fixes neutral :: "'a" ("\<zero>")
assumes neutl: "\<zero> \<oplus> x = x"
text \<open>\noindent Again, we prove some instances, by providing
@@ -140,7 +140,7 @@
text \<open>\noindent To finish our small algebra example, we add a \<open>group\<close> class:\<close>
class group = monoidl +
- fixes inv :: "'a \<Rightarrow> 'a" (\<open>\<div> _\<close> [81] 80)
+ fixes inv :: "'a \<Rightarrow> 'a" ("\<div> _" [81] 80)
assumes invl: "\<div> x \<oplus> x = \<zero>"
text \<open>\noindent We continue with a further example for abstract
--- a/src/Doc/Tutorial/Types/Overloading.thy Fri Sep 27 22:44:30 2024 +0200
+++ b/src/Doc/Tutorial/Types/Overloading.thy Fri Sep 27 23:47:45 2024 +0200
@@ -11,7 +11,7 @@
for arbitrary types by means of a type class:\<close>
class plus =
- fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl \<open>\<oplus>\<close> 70)
+ fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<oplus>" 70)
text \<open>\noindent This introduces a new class @{class [source] plus},
along with a constant @{const [source] plus} with nice infix syntax.