# 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 \ ty \ pname \ bool" ("_ \ _ accessible'_in _" [61,61,61] 60) and - rt_accessible_in :: "prog \ ref_ty \ pname \ bool" ("_ \ _ accessible'_in' _" [61,61,61] 60) + rt_accessible_in :: "prog \ ref_ty \ pname \ bool" ("_ \ _ accessible'_in'' _" [61,61,61] 60) where "G\(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] \ bool" - ("_ \ _ <=' _" [71,71] 70) where + ("_ \ _ <='' _" [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 \ (\i. i \ I \ (P)\<^sub>F i \ A i) } " syntax - "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\' _\_./ _)" 10) + "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\'' _\_./ _)" 10) translations "\' x\A. B" == "CONST Pi' A (\x. B)"