# HG changeset patch
# User wenzelm
# Date 1727014729 -7200
# Node ID 92d2ceda2370bf1e5b65a43f5c7994073065d5dc
# Parent  6c9628a116ccaec568cfe289743a5d093a3f0d4e
tuned comments;

diff -r 6c9628a116cc -r 92d2ceda2370 src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Sun Sep 22 16:12:15 2024 +0200
+++ b/src/Sequents/LK0.thy	Sun Sep 22 16:18:49 2024 +0200
@@ -45,7 +45,7 @@
 
 axiomatization where
 
-  (*Structural rules: contraction, thinning, exchange [Soren Heilmann] *)
+  (*Structural rules: contraction, thinning, exchange [Søren Heilmann] *)
 
   contRS: "$H \<turnstile> $E, $S, $S, $F \<Longrightarrow> $H \<turnstile> $E, $S, $F" and
   contLS: "$H, $S, $S, $G \<turnstile> $E \<Longrightarrow> $H, $S, $G \<turnstile> $E" and
diff -r 6c9628a116cc -r 92d2ceda2370 src/Sequents/simpdata.ML
--- a/src/Sequents/simpdata.ML	Sun Sep 22 16:12:15 2024 +0200
+++ b/src/Sequents/simpdata.ML	Sun Sep 22 16:18:49 2024 +0200
@@ -4,7 +4,7 @@
 
 Instantiation of the generic simplifier for LK.
 
-Borrows from the DC simplifier of Soren Heilmann.
+Borrows from the DC simplifier of Søren Heilmann (see http://www.sth.dk/sth).
 *)