--- a/NEWS Fri Mar 13 16:12:50 2020 +0100
+++ b/NEWS Fri Mar 13 23:25:34 2020 +0100
@@ -41,7 +41,8 @@
* Mixfix annotations may use "' " (single quote followed by space) to
separate delimiters (as documented in the isar-ref manual), without
-requiring an auxiliary empty block.
+requiring an auxiliary empty block. A literal single quote needs to be
+escaped properly: rare INCOMPATIBILITY.
*** Isar ***
--- a/src/HOL/Bali/DeclConcepts.thy Fri Mar 13 16:12:50 2020 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy Fri Mar 13 23:25:34 2020 +0100
@@ -23,7 +23,7 @@
primrec
accessible_in :: "prog \<Rightarrow> ty \<Rightarrow> pname \<Rightarrow> bool" ("_ \<turnstile> _ accessible'_in _" [61,61,61] 60) and
- rt_accessible_in :: "prog \<Rightarrow> ref_ty \<Rightarrow> pname \<Rightarrow> bool" ("_ \<turnstile> _ accessible'_in' _" [61,61,61] 60)
+ rt_accessible_in :: "prog \<Rightarrow> ref_ty \<Rightarrow> pname \<Rightarrow> bool" ("_ \<turnstile> _ accessible'_in'' _" [61,61,61] 60)
where
"G\<turnstile>(PrimT p) accessible_in pack = True"
| accessible_in_RefT_simp:
--- a/src/HOL/MicroJava/BV/JVMType.thy Fri Mar 13 16:12:50 2020 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy Fri Mar 13 23:25:34 2020 +0100
@@ -50,7 +50,7 @@
"sup_state G == Product.le (Listn.le (subtype G)) (sup_loc G)"
definition sup_state_opt :: "['code prog,state_type option,state_type option] \<Rightarrow> bool"
- ("_ \<turnstile> _ <=' _" [71,71] 70) where
+ ("_ \<turnstile> _ <='' _" [71,71] 70) where
"sup_state_opt G == Opt.le (sup_state G)"
--- a/src/HOL/Probability/Fin_Map.thy Fri Mar 13 16:12:50 2020 +0100
+++ b/src/HOL/Probability/Fin_Map.thy Fri Mar 13 23:25:34 2020 +0100
@@ -89,7 +89,7 @@
"Pi' I A = { P. domain P = I \<and> (\<forall>i. i \<in> I \<longrightarrow> (P)\<^sub>F i \<in> A i) } "
syntax
- "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi>' _\<in>_./ _)" 10)
+ "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi>'' _\<in>_./ _)" 10)
translations
"\<Pi>' x\<in>A. B" == "CONST Pi' A (\<lambda>x. B)"