--- a/doc-src/IsarRef/Thy/First_Order_Logic.thy Thu Feb 12 11:19:54 2009 +0100
+++ b/doc-src/IsarRef/Thy/First_Order_Logic.thy Thu Feb 12 11:36:15 2009 +0100
@@ -6,11 +6,11 @@
begin
text {*
- In order to commence a new object-logic within Isabelle/Pure we
- introduce abstract syntactic categories @{text "i"} for individuals
- and @{text "o"} for object-propositions. The latter is embedded
- into the language of Pure propositions by means of a separate
- judgment.
+ \noindent In order to commence a new object-logic within
+ Isabelle/Pure we introduce abstract syntactic categories @{text "i"}
+ for individuals and @{text "o"} for object-propositions. The latter
+ is embedded into the language of Pure propositions by means of a
+ separate judgment.
*}
typedecl i
@@ -124,9 +124,9 @@
qed
text {*
- Reasoning from basic axioms is often tedious. Our proofs work by
- producing various instances of the given rules (potentially the
- symmetric form) using the pattern ``@{command have}~@{text
+ \noindent Reasoning from basic axioms is often tedious. Our proofs
+ work by producing various instances of the given rules (potentially
+ the symmetric form) using the pattern ``@{command have}~@{text
eq}~@{command "by"}~@{text "(rule r)"}'' and composing the chain of
results via @{command also}/@{command finally}. These steps may
involve any of the transitivity rules declared in
@@ -160,7 +160,7 @@
definitions in order to normalize each equational problem. A more
realistic object-logic would include proper setup for the Simplifier
(\secref{sec:simplifier}), the main automated tool for equational
- reasoning in Isabelle. Then ``@{command unfolding}~@{text
+ reasoning in Isabelle. Then ``@{command unfolding}~@{thm
left_inv}~@{command ".."}'' would become ``@{command "by"}~@{text
"(simp add: left_inv)"}'' etc.
*}
@@ -173,7 +173,7 @@
text {*
We axiomatize basic connectives of propositional logic: implication,
disjunction, and conjunction. The associated rules are modeled
- after Gentzen's natural deduction \cite{Gentzen:1935}.
+ after Gentzen's system of Natural Deduction \cite{Gentzen:1935}.
*}
axiomatization
@@ -226,9 +226,9 @@
(*>*)
text {*
- Note that the analogous elimination for disjunction ``@{text
- "\<ASSUMES> A \<or> B \<OBTAINS> A \<BBAR> B"}'' coincides with the
- original axiomatization of @{text "disjE"}.
+ \noindent Note that the analogous elimination rule for disjunction
+ ``@{text "\<ASSUMES> A \<or> B \<OBTAINS> A \<BBAR> B"}'' coincides with
+ the original axiomatization of @{thm disjE}.
\medskip We continue propositional logic by introducing absurdity
with its characteristic elimination. Plain truth may then be
@@ -247,7 +247,8 @@
unfolding true_def ..
text {*
- \medskip Now negation represents an implication towards absurdity:
+ \medskip\noindent Now negation represents an implication towards
+ absurdity:
*}
definition
@@ -314,9 +315,9 @@
propositional proofs in general. All three rules characterize
classical logic independently, but the original rule is already the
most convenient to use, because it leaves the conclusion unchanged.
- Note that @{text "(\<not> C \<Longrightarrow> C) \<Longrightarrow> C"} fits again into our format for
+ Note that @{prop "(\<not> C \<Longrightarrow> C) \<Longrightarrow> C"} fits again into our format for
eliminations, despite the additional twist that the context refers
- to the main conclusion. So we may write @{text "classical"} as the
+ to the main conclusion. So we may write @{thm classical} as the
Isar statement ``@{text "\<OBTAINS> \<not> thesis"}''. This also
explains nicely how classical reasoning really works: whatever the
main @{text thesis} might be, we may always assume its negation!
@@ -332,8 +333,8 @@
of the underlying framework. According to the well-known technique
introduced by Church \cite{church40}, quantifiers are operators on
predicates, which are syntactically represented as @{text "\<lambda>"}-terms
- of type @{text "i \<Rightarrow> o"}. Specific binder notation relates @{text
- "All (\<lambda>x. B x)"} to @{text "\<forall>x. B x"} etc.
+ of type @{typ "i \<Rightarrow> o"}. Binder notation turns @{text "All (\<lambda>x. B
+ x)"} into @{text "\<forall>x. B x"} etc.
*}
axiomatization
--- a/doc-src/IsarRef/Thy/Framework.thy Thu Feb 12 11:19:54 2009 +0100
+++ b/doc-src/IsarRef/Thy/Framework.thy Thu Feb 12 11:36:15 2009 +0100
@@ -886,10 +886,10 @@
The present Isar infrastructure is sufficiently flexible to support
calculational reasoning (chains of transitivity steps) as derived
concept. The generic proof elements introduced below depend on
- rules declared as @{text "[trans]"} in the context. It is left to
+ rules declared as @{attribute trans} in the context. It is left to
the object-logic to provide a suitable rule collection for mixed
- @{text "="}, @{text "<"}, @{text "\<le>"}, @{text "\<subset>"}, @{text "\<subseteq>"} etc.
- Due to the flexibility of rule composition
+ relations of @{text "="}, @{text "<"}, @{text "\<le>"}, @{text "\<subset>"},
+ @{text "\<subseteq>"} etc. Due to the flexibility of rule composition
(\secref{sec:framework-resolution}), substitution of equals by
equals is covered as well, even substitution of inequalities
involving monotonicity conditions; see also \cite[\S6]{Wenzel-PhD}
@@ -902,10 +902,10 @@
selected from the context. The course of reasoning is organized by
maintaining a secondary fact called ``@{fact calculation}'', apart
from the primary ``@{fact this}'' already provided by the Isar
- primitives. In the definitions below, @{attribute OF} is
+ primitives. In the definitions below, @{attribute OF} refers to
@{inference resolution} (\secref{sec:framework-resolution}) with
- multiple rule arguments, and @{text "trans"} refers to a suitable
- rule from the context:
+ multiple rule arguments, and @{text "trans"} represents to a
+ suitable rule from the context:
\begin{matharray}{rcl}
@{command "also"}@{text "\<^sub>0"} & \equiv & @{command "note"}~@{text "calculation = this"} \\