# HG changeset patch
# User wenzelm
# Date 1584138334 -3600
# Node ID d350aabace23953cc9dda9b644c1a2c432ba926d
# Parent  4dd5dadfc87dbf37e6838c0567b948aa67c68495
proper escape for literal single quotes;

diff -r 4dd5dadfc87d -r d350aabace23 NEWS
--- 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 ***
diff -r 4dd5dadfc87d -r d350aabace23 src/HOL/Bali/DeclConcepts.thy
--- 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:
diff -r 4dd5dadfc87d -r d350aabace23 src/HOL/MicroJava/BV/JVMType.thy
--- 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)"
 
 
diff -r 4dd5dadfc87d -r d350aabace23 src/HOL/Probability/Fin_Map.thy
--- 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)"