# HG changeset patch
# User wenzelm
# Date 1542313980 -3600
# Node ID 196347d2fd2da791fbb7b8e48d58e20415c7c406
# Parent  341ebf35464b4b09955e26237a1088c0d63b0075
proper citation (amending 98ba42f19995);

diff -r 341ebf35464b -r 196347d2fd2d src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Wed Nov 14 22:13:57 2018 +0100
+++ b/src/Doc/Implementation/Logic.thy	Thu Nov 15 21:33:00 2018 +0100
@@ -892,8 +892,8 @@
 text \<open>
   The idea of object-level rules is to model Natural Deduction inferences in
   the style of Gentzen @{cite "Gentzen:1935"}, but we allow arbitrary nesting
-  similar to @{cite extensions91}. The most basic rule format is that of a
-  \<^emph>\<open>Horn Clause\<close>:
+  similar to @{cite "Schroeder-Heister:1984"}. The most basic rule format is
+  that of a \<^emph>\<open>Horn Clause\<close>:
   \[
   \infer{\<open>A\<close>}{\<open>A\<^sub>1\<close> & \<open>\<dots>\<close> & \<open>A\<^sub>n\<close>}
   \]