# HG changeset patch
# User wenzelm
# Date 1727473665 -7200
# Node ID 2cc651d3ce8ed78de991439c461736575e2a8208
# Parent  7638776e097724b474e8e69d238b83d7edeab60a
partial revert of d97fdabd9e2b, to build old documentation more reliably;

diff -r 7638776e0977 -r 2cc651d3ce8e src/Doc/Tutorial/CTL/CTL.thy
--- 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)" |
diff -r 7638776e0977 -r 2cc651d3ce8e src/Doc/Tutorial/CTL/PDL.thy
--- 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))" |
diff -r 7638776e0977 -r 2cc651d3ce8e src/Doc/Tutorial/Documents/Documents.thy
--- 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.
diff -r 7638776e0977 -r 2cc651d3ce8e src/Doc/Tutorial/Inductive/Star.thy
--- 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*"
diff -r 7638776e0977 -r 2cc651d3ce8e src/Doc/Tutorial/Misc/fakenat.thy
--- 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
 (*>*)
diff -r 7638776e0977 -r 2cc651d3ce8e src/Doc/Tutorial/Protocol/Message.thy
--- 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
diff -r 7638776e0977 -r 2cc651d3ce8e src/Doc/Tutorial/ToyList/ToyList.thy
--- 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)"
 
diff -r 7638776e0977 -r 2cc651d3ce8e src/Doc/Tutorial/Types/Axioms.thy
--- 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
diff -r 7638776e0977 -r 2cc651d3ce8e src/Doc/Tutorial/Types/Overloading.thy
--- 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.