summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 15 Apr 2014 20:24:49 +0200 | |

changeset 56594 | e3a06699a13f |

parent 56593 | 0ea7c84110ac |

child 56595 | 82be272f7916 |

tuned spelling;

--- 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.