--- a/src/Doc/Isar_Ref/First_Order_Logic.thy Sun Oct 05 22:22:40 2014 +0200
+++ b/src/Doc/Isar_Ref/First_Order_Logic.thy Sun Oct 05 22:24:07 2014 +0200
@@ -174,7 +174,7 @@
text {*
We axiomatize basic connectives of propositional logic: implication,
disjunction, and conjunction. The associated rules are modeled
- after Gentzen's system of Natural Deduction \cite{Gentzen:1935}.
+ after Gentzen's system of Natural Deduction @{cite "Gentzen:1935"}.
*}
axiomatization
@@ -333,7 +333,7 @@
text {*
Representing quantifiers is easy, thanks to the higher-order nature
of the underlying framework. According to the well-known technique
- introduced by Church \cite{church40}, quantifiers are operators on
+ introduced by Church @{cite "church40"}, quantifiers are operators on
predicates, which are syntactically represented as @{text "\<lambda>"}-terms
of type @{typ "i \<Rightarrow> o"}. Binder notation turns @{text "All (\<lambda>x. B
x)"} into @{text "\<forall>x. B x"} etc.