# HG changeset patch # User wenzelm # Date 1397586289 -7200 # Node ID e3a06699a13fc23dd3061c93c415998c8acf47b3 # Parent 0ea7c84110ac969931e97faf981592824cecc620 tuned spelling; diff -r 0ea7c84110ac -r e3a06699a13f src/Doc/Implementation/Integration.thy --- 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 diff -r 0ea7c84110ac -r e3a06699a13f src/Doc/Implementation/ML.thy --- 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: \\<^sub>1 \ \\<^sub>2 \ \"} can be applied to @{text "x: \\<^sub>1"} and the remaining @{text "(f x): \\<^sub>2 \ \"} passed to another function etc. How well this works in practice depends on the order of diff -r 0ea7c84110ac -r e3a06699a13f src/Doc/Isar_Ref/Document_Preparation.thy --- 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. *} diff -r 0ea7c84110ac -r e3a06699a13f src/Doc/Isar_Ref/First_Order_Logic.thy --- 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 \ 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 "\A. PROP A \ PROP A" proof - assume [symmetric, defn]: "\x y. (x \ y) \ Trueprop (x = y)" + fix x (*>*) have "x \ 1 = x \ (x\ \ x)" unfolding left_inv .. also have "\ = (x \ x\) \ x" unfolding assoc .. diff -r 0ea7c84110ac -r e3a06699a13f src/Doc/Isar_Ref/Framework.thy --- 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 the nested reasoning. This kind of diff -r 0ea7c84110ac -r e3a06699a13f src/Doc/Isar_Ref/Generic.thy --- 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 \ ?Q\<^sub>1 \ (?Q\<^sub>1 \ ?P\<^sub>2 \ ?Q\<^sub>2) \ (?P\<^sub>1 \ ?P\<^sub>2) \ (?Q\<^sub>1 \ ?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 \ 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 diff -r 0ea7c84110ac -r e3a06699a13f src/Doc/Isar_Ref/Spec.thy --- 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 \ 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 :: \ decl"} may be defined separately on type instances @{text "c :: (\\<^sub>1, \, \\<^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.