diff -r 8bb064045b4e -r e51c9a67a68d thys/Journal/Paper.thy
--- a/thys/Journal/Paper.thy	Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/Journal/Paper.thy	Sun Oct 10 00:56:47 2021 +0100
@@ -5,7 +5,7 @@
    "../Simplifying" 
    "../Positions"
    "../Sulzmann"
-   "~~/src/HOL/Library/LaTeXsugar"
+   "HOL-Library.LaTeXsugar"
 begin
 
 lemma Suc_0_fold:
@@ -50,7 +50,7 @@
 
   ZERO ("\<^bold>0" 81) and 
   ONE ("\<^bold>1" 81) and 
-  CHAR ("_" [1000] 80) and
+  CH ("_" [1000] 80) and
   ALT ("_ + _" [77,77] 78) and
   SEQ ("_ \<cdot> _" [77,77] 78) and
   STAR ("_\<^sup>\<star>" [79] 78) and
@@ -333,7 +333,7 @@
   \<open>r :=\<close>
   @{const "ZERO"} $\mid$
   @{const "ONE"} $\mid$
-  @{term "CHAR c"} $\mid$
+  @{term "CH c"} $\mid$
   @{term "ALT r\<^sub>1 r\<^sub>2"} $\mid$
   @{term "SEQ r\<^sub>1 r\<^sub>2"} $\mid$
   @{term "STAR r"} 
@@ -1411,7 +1411,7 @@
 \begin{tabular}{lcl}
   @{term areg} & $::=$ & @{term "AZERO"}\\
                & $\mid$ & @{term "AONE bs"}\\
-               & $\mid$ & @{term "ACHAR bs c"}\\
+               & $\mid$ & @{term "ACH bs c"}\\
                & $\mid$ & @{term "AALT bs r\<^sub>1 r\<^sub>2"}\\
                & $\mid$ & @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}\\
                & $\mid$ & @{term "ASTAR bs r"}
@@ -1693,7 +1693,7 @@
   By induction on the definition of @{term "erase r"}. The cases for rule 1) and 2) are
   straightforward as @{term "der c ZERO"} and @{term "der c ONE"} are both equal to 
   @{term ZERO}. This means @{term "\<Turnstile> v : ZERO"} cannot hold. Similarly in case of rule 3)
-  where @{term r} is of the form @{term "ACHAR d"} with @{term "c = d"}. Then by assumption
+  where @{term r} is of the form @{term "ACH d"} with @{term "c = d"}. Then by assumption
   we know @{term "\<Turnstile> v : ONE"}, which implies @{term "v = Void"}. The equation follows by 
   simplification of left- and right-hand side. In  case @{term "c \<noteq> d"} we have again
   @{term "\<Turnstile> v : ZERO"}, which cannot  hold.