# HG changeset patch # User wenzelm # Date 1210789901 -7200 # Node ID d066f9db833b0c19863a920ebd9c11dbd24372e6 # Parent 1120f6cc10b011006bdcf59e0794cd64594851c4 updated generated file; diff -r 1120f6cc10b0 -r d066f9db833b doc-src/IsarRef/Thy/document/Generic.tex --- 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}% diff -r 1120f6cc10b0 -r d066f9db833b doc-src/IsarRef/Thy/document/HOL_Specific.tex --- 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.% diff -r 1120f6cc10b0 -r d066f9db833b doc-src/IsarRef/Thy/document/Proof.tex --- 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, diff -r 1120f6cc10b0 -r d066f9db833b doc-src/IsarRef/Thy/document/ZF_Specific.tex --- 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}% diff -r 1120f6cc10b0 -r d066f9db833b doc-src/IsarRef/Thy/document/pure.tex --- 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