Automatically replace old LF symbols and delimiters

source/test.mmt

@@ -22,7 +22,7 @@ theory Basics =
 
 theory Pi : ?Basics =
 	pi # { V1T ,… } 2 prec -10000 ❙
-	arrow # 1⟶… prec -9999 ❙
+	arrow # 1→… prec -9999 ❙
     apply1  # 1%w… prec -10 ❙
 	apply2 # 1 ( 2,… ) prec -100000 ❙
 	lambda # [ V1T ,… ] 2 prec -10000 ❙
@@ -80,10 +80,10 @@ theory Mod : ?Basics =
 
 theory Term : ?Basics =
 	// copy paste ❙
-	formation # {| 1 |} 2 prec -10000
-	reflect   # ⌜ 1 : 2 ⌝ prec -10000
-	eval      # ⌞ 1 ⌟ 2   prec -10000
-	elim      # 1 ^ 2     prec -10000
+	formation # {| 1 |} 2 prec -10000❙
+	reflect   # ⌜ 1 : 2 ⌝ prec -10000❙
+	eval      # ⌞ 1 ⌟ 2   prec -10000❙
+	elim      # 1 ^ 2     prec -10000❙
 ❚
 
 theory FiniteSet : ?Basics =
@@ -108,7 +108,7 @@ theory MultiSet : ?Basics =
 
 theory InfiniteSequences : ?Basics =
 	// pretty much identical to finite sequences, notationwise. Probably additional introduction
-	form via ℕ ⟶ A or induction? ❙
+	form via ℕ → A or induction? ❙
 	infseq # 1 ^≤ω ❙
 	nil # nil %I1 ❙
 	cons # 1 :: 2 ❙