fiddling

src/plta/Fonts.lagda

@@ -40,6 +40,11 @@ ABCDEFGHIJKLMNOPQRSTUVWXYZ|
 →→→→
 ↦↦↦↦
 ↠↠↠↠
+⊢⊢⊢⊢
+⊣⊣⊣⊣
+∈∈∈∈
+∋∋∋∋
+----
 -}
 \end{code}
 
@@ -71,3 +76,8 @@ Indented code:
     →→→→
     ↦↦↦↦
     ↠↠↠↠
+    ⊢⊢⊢⊢
+    ⊣⊣⊣⊣
+    ∈∈∈∈
+    ∋∋∋∋
+    ----

src/plta/Lambda.lagda

@@ -8,9 +8,10 @@ permalink : /Lambda/
 module plta.Lambda where
 \end{code}
 
-[Parts of this chapter take their text from chapter _Stlc_
+[This chapter was originally based on Chapter _Stlc_
 of _Software Foundations_ (_Programming Language Foundations_).
-Those parts will be revised.]
+It has now been updated, but if you catch any unintended
+copying please let me know.]
 
 The _lambda-calculus_, first published by the logician Alonzo Church in
 1932, is a core calculus with only three syntactic constructs: