From 5d122b932f9a158c94c2325d69f6388de276582e Mon Sep 17 00:00:00 2001
From: Tom Wiesing <tom.wiesing@fau.de>
Date: Thu, 5 Apr 2018 14:22:04 +0200
Subject: [PATCH] Automatically replace old LF symbols and delimiters

---
 source/test.mmt | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/source/test.mmt b/source/test.mmt
index 3b3fa88..37dd630 100644
--- a/source/test.mmt
+++ b/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 ❙
-- 
GitLab