--- a/doc-src/IsarRef/Thy/document/Generic.tex Wed May 14 20:31:17 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Wed May 14 20:31:41 2008 +0200
@@ -11,7 +11,7 @@
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Generic\isanewline
-\isakeyword{imports}\ CPure\isanewline
+\isakeyword{imports}\ Main\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed May 14 20:31:17 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed May 14 20:31:41 2008 +0200
@@ -69,9 +69,10 @@
corresponding injection/surjection pair (in both directions). Rules
\isa{Rep{\isacharunderscore}t{\isacharunderscore}inject} and \isa{Abs{\isacharunderscore}t{\isacharunderscore}inject} provide a slightly
more convenient view on the injectivity part, suitable for automated
- proof tools (e.g.\ in \mbox{\isa{simp}} or \mbox{\isa{iff}} declarations).
- Rules \isa{Rep{\isacharunderscore}t{\isacharunderscore}cases}/\isa{Rep{\isacharunderscore}t{\isacharunderscore}induct}, and \isa{Abs{\isacharunderscore}t{\isacharunderscore}cases}/\isa{Abs{\isacharunderscore}t{\isacharunderscore}induct} provide alternative views on
- surjectivity; these are already declared as set or type rules for
+ proof tools (e.g.\ in \mbox{\isa{simp}} or \mbox{\isa{iff}}
+ declarations). Rules \isa{Rep{\isacharunderscore}t{\isacharunderscore}cases}/\isa{Rep{\isacharunderscore}t{\isacharunderscore}induct}, and
+ \isa{Abs{\isacharunderscore}t{\isacharunderscore}cases}/\isa{Abs{\isacharunderscore}t{\isacharunderscore}induct} provide alternative views
+ on surjectivity; these are already declared as set or type rules for
the generic \mbox{\isa{cases}} and \mbox{\isa{induct}} methods.
An alternative name may be specified in parentheses; the default is
@@ -817,15 +818,15 @@
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{HOL}{method}{arith}\mbox{\isa{arith}} & : & \isarmeth \\
- \indexdef{HOL}{method}{arith\_split}\mbox{\isa{arith{\isacharunderscore}split}} & : & \isaratt \\
+ \indexdef{HOL}{attribute}{arith\_split}\mbox{\isa{arith{\isacharunderscore}split}} & : & \isaratt \\
\end{matharray}
The \mbox{\isa{arith}} method decides linear arithmetic problems
(on types \isa{nat}, \isa{int}, \isa{real}). Any current
facts are inserted into the goal before running the procedure.
- The \mbox{\isa{arith{\isacharunderscore}split}} attribute declares case split rules
- to be expanded before the arithmetic procedure is invoked.
+ The \mbox{\isa{arith{\isacharunderscore}split}} attribute declares case split
+ rules to be expanded before the arithmetic procedure is invoked.
Note that a simpler (but faster) version of arithmetic reasoning is
already performed by the Simplifier.%
--- a/doc-src/IsarRef/Thy/document/Proof.tex Wed May 14 20:31:17 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Wed May 14 20:31:41 2008 +0200
@@ -601,9 +601,10 @@
\item [\mbox{\isa{of}}~\isa{{\isachardoublequote}t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isachardoublequote}}] performs
positional instantiation of term variables. The terms \isa{{\isachardoublequote}t\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ t\isactrlsub n{\isachardoublequote}} are substituted for any schematic
- variables occurring in a theorem from left to right; ``\isa{{\isacharunderscore}}'' (underscore) indicates to skip a position. Arguments following
- a ``\mbox{\isa{\isakeyword{concl}}}\isa{{\isachardoublequote}{\isacharcolon}{\isachardoublequote}}'' specification refer to positions
- of the conclusion of a rule.
+ variables occurring in a theorem from left to right; ``\isa{{\isacharunderscore}}''
+ (underscore) indicates to skip a position. Arguments following a
+ ``\isa{{\isachardoublequote}concl{\isacharcolon}{\isachardoublequote}}'' specification refer to positions of the
+ conclusion of a rule.
\item [\mbox{\isa{where}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ x\isactrlsub n\ {\isacharequal}\ t\isactrlsub n{\isachardoublequote}}] performs named instantiation of schematic
type and term variables occurring in a theorem. Schematic variables
@@ -775,7 +776,7 @@
multi-step tactic script for \mbox{\isa{\isacommand{qed}}}, but may be given
anywhere within the proof body.
- No facts are passed to \mbox{\isa{m}} here. Furthermore, the static
+ No facts are passed to \isa{m} here. Furthermore, the static
context is that of the enclosing goal (as for actual \mbox{\isa{\isacommand{qed}}}). Thus the proof method may not refer to any assumptions
introduced in the current body, for example.
@@ -1001,7 +1002,7 @@
\item [\mbox{\isa{trans}}] declares theorems as transitivity rules.
\item [\mbox{\isa{sym}}] declares symmetry rules, as well as
- \mbox{\isa{Pure{\isachardot}elim{\isacharquery}}} rules.
+ \mbox{\isa{Pure{\isachardot}elim}}\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}} rules.
\item [\mbox{\isa{symmetric}}] resolves a theorem with some rule
declared as \mbox{\isa{sym}} in the current context. For example,
--- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex Wed May 14 20:31:17 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex Wed May 14 20:31:41 2008 +0200
@@ -11,7 +11,7 @@
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ ZF{\isacharunderscore}Specific\isanewline
-\isakeyword{imports}\ ZF\isanewline
+\isakeyword{imports}\ Main\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
--- a/doc-src/IsarRef/Thy/document/pure.tex Wed May 14 20:31:17 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/pure.tex Wed May 14 20:31:41 2008 +0200
@@ -753,7 +753,7 @@
\indexdef{}{command}{print\_attributes}\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\indexdef{}{command}{print\_theorems}\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\indexdef{}{command}{find\_theorems}\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
- \indexdef{}{command}{thms\_deps}\mbox{\isa{\isacommand{thms{\isacharunderscore}deps}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{thm\_deps}\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\indexdef{}{command}{print\_facts}\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
\indexdef{}{command}{print\_binds}\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
\end{matharray}
@@ -816,7 +816,7 @@
yields \emph{all} currently known facts. An optional limit for the
number of printed facts may be given; the default is 40. By
default, duplicates are removed from the search result. Use
- \mbox{\isa{\isakeyword{with{\isacharunderscore}dups}}} to display duplicates.
+ \isa{with{\isacharunderscore}dups} to display duplicates.
\item [\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}]
visualizes dependencies of facts, using Isabelle's graph browser