Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned comments;
authorwenzelm
Sun, 22 Sep 2024 16:18:49 +0200
changeset 80924 92d2ceda2370
parent 80923 6c9628a116cc
child 80925 6c1146e6e79e
tuned comments;
src/Sequents/LK0.thy file | annotate | diff | comparison | revisions
src/Sequents/simpdata.ML file | annotate | diff | comparison | revisions 
--- 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
--- 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).
 *)
isabelle