--- a/src/Doc/Implementation/Integration.thy Tue Apr 15 19:51:55 2014 +0200
+++ b/src/Doc/Implementation/Integration.thy Tue Apr 15 20:24:49 2014 +0200
@@ -184,6 +184,8 @@
section {* Theory database \label{sec:theory-database} *}
text {*
+ %FIXME update
+
The theory database maintains a collection of theories, together
with some administrative information about their original sources,
which are held in an external store (i.e.\ some directory within the
--- a/src/Doc/Implementation/ML.thy Tue Apr 15 19:51:55 2014 +0200
+++ b/src/Doc/Implementation/ML.thy Tue Apr 15 20:24:49 2014 +0200
@@ -758,7 +758,7 @@
the redundant tuple structure needs to be accommodated by formal
reasoning.}
- Currying gives some flexiblity due to \emph{partial application}. A
+ Currying gives some flexibility due to \emph{partial application}. A
function @{text "f: \<tau>\<^sub>1 \<rightarrow> \<tau>\<^sub>2 \<rightarrow> \<tau>"} can be applied to @{text "x: \<tau>\<^sub>1"}
and the remaining @{text "(f x): \<tau>\<^sub>2 \<rightarrow> \<tau>"} passed to another function
etc. How well this works in practice depends on the order of
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Tue Apr 15 19:51:55 2014 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Tue Apr 15 20:24:49 2014 +0200
@@ -394,7 +394,7 @@
\end{description}
- For boolean flags, ``@{text "name = true"}'' may be abbreviated as
+ For Boolean flags, ``@{text "name = true"}'' may be abbreviated as
``@{text name}''. All of the above flags are disabled by default,
unless changed specifically for a logic session in the corresponding
@{verbatim "ROOT"} file. *}
--- a/src/Doc/Isar_Ref/First_Order_Logic.thy Tue Apr 15 19:51:55 2014 +0200
+++ b/src/Doc/Isar_Ref/First_Order_Logic.thy Tue Apr 15 20:24:49 2014 +0200
@@ -20,7 +20,7 @@
Trueprop :: "o \<Rightarrow> prop" ("_" 5)
text {*
- \noindent Note that the object-logic judgement is implicit in the
+ \noindent Note that the object-logic judgment is implicit in the
syntax: writing @{prop A} produces @{term "Trueprop A"} internally.
From the Pure perspective this means ``@{prop A} is derivable in the
object-logic''.
@@ -145,6 +145,7 @@
theorem "\<And>A. PROP A \<Longrightarrow> PROP A"
proof -
assume [symmetric, defn]: "\<And>x y. (x \<equiv> y) \<equiv> Trueprop (x = y)"
+ fix x
(*>*)
have "x \<circ> 1 = x \<circ> (x\<inverse> \<circ> x)" unfolding left_inv ..
also have "\<dots> = (x \<circ> x\<inverse>) \<circ> x" unfolding assoc ..
--- a/src/Doc/Isar_Ref/Framework.thy Tue Apr 15 19:51:55 2014 +0200
+++ b/src/Doc/Isar_Ref/Framework.thy Tue Apr 15 20:24:49 2014 +0200
@@ -154,7 +154,7 @@
text {*
\medskip\noindent This Isar reasoning pattern again refers to the
primitive rule depicted above. The system determines it in the
- ``@{command proof}'' step, which could have been spelt out more
+ ``@{command proof}'' step, which could have been spelled out more
explicitly as ``@{command proof}~@{text "(rule InterI)"}''. Note
that the rule involves both a local parameter @{term "A"} and an
assumption @{prop "A \<in> \<A>"} in the nested reasoning. This kind of
--- a/src/Doc/Isar_Ref/Generic.thy Tue Apr 15 19:51:55 2014 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy Tue Apr 15 20:24:49 2014 +0200
@@ -682,7 +682,7 @@
assumptions: @{text [display] "?P\<^sub>1 \<longleftrightarrow> ?Q\<^sub>1 \<Longrightarrow> (?Q\<^sub>1 \<Longrightarrow> ?P\<^sub>2 \<longleftrightarrow> ?Q\<^sub>2) \<Longrightarrow>
(?P\<^sub>1 \<longrightarrow> ?P\<^sub>2) \<longleftrightarrow> (?Q\<^sub>1 \<longrightarrow> ?Q\<^sub>2)"}
- Given this rule, the simplifier assumes @{text "?Q\<^sub>1"} and extracts
+ Given this rule, the Simplifier assumes @{text "?Q\<^sub>1"} and extracts
rewrite rules from it when simplifying @{text "?P\<^sub>2"}. Such local
assumptions are effective for rewriting formulae such as @{text "x =
0 \<longrightarrow> y + x = y"}.
@@ -843,7 +843,7 @@
text {* Martin and Nipkow \cite{martin-nipkow} discuss the theory and
give many examples; other algebraic structures are amenable to
- ordered rewriting, such as boolean rings. The Boyer-Moore theorem
+ ordered rewriting, such as Boolean rings. The Boyer-Moore theorem
prover \cite{bm88book} also employs ordered rewriting.
*}
@@ -961,7 +961,7 @@
[source=false, show_types] unit_eq} in HOL performs fine-grained
control over rule application, beyond higher-order pattern matching.
Declaring @{thm unit_eq} as @{attribute simp} directly would make
- the simplifier loop! Note that a version of this simplification
+ the Simplifier loop! Note that a version of this simplification
procedure is already active in Isabelle/HOL. *}
simproc_setup unit ("x::unit") = {*
@@ -1239,7 +1239,7 @@
conclusion; the options @{text no_asm} etc.\ tune the Simplifier in
the same way as the for the @{text simp} method.
- Note that forward simplification restricts the simplifier to its
+ Note that forward simplification restricts the Simplifier to its
most basic operation of term rewriting; solver and looper tactics
(\secref{sec:simp-strategies}) are \emph{not} involved here. The
@{attribute simplified} attribute should be only rarely required
--- a/src/Doc/Isar_Ref/Spec.thy Tue Apr 15 19:51:55 2014 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Tue Apr 15 20:24:49 2014 +0200
@@ -861,11 +861,11 @@
@{text d} is proven to be subclass @{text c} and the locale @{text
c} is interpreted into @{text d} simultaneously.
- A weakend form of this is available through a further variant of
+ A weakened form of this is available through a further variant of
@{command instance}: @{command instance}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} opens
a proof that class @{text "c\<^sub>2"} implies @{text "c\<^sub>1"} without reference
to the underlying locales; this is useful if the properties to prove
- the logical connection are not sufficent on the locale level but on
+ the logical connection are not sufficient on the locale level but on
the theory level.
\item @{command "print_classes"} prints all classes in the current
@@ -961,7 +961,7 @@
constant being declared as @{text "c :: \<alpha> decl"} may be
defined separately on type instances
@{text "c :: (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t decl"}
- for each type constructor @{text t}. At most occassions
+ for each type constructor @{text t}. At most occasions
overloading will be used in a Haskell-like fashion together with
type classes by means of @{command "instantiation"} (see
\secref{sec:class}). Sometimes low-level overloading is desirable.