1.1 --- a/doc-src/IsarRef/Thy/Proof.thy Mon May 02 20:14:19 2011 +0200
1.2 +++ b/doc-src/IsarRef/Thy/Proof.thy Mon May 02 20:34:34 2011 +0200
1.3 @@ -339,7 +339,7 @@
1.4 facts in order to establish the goal to be claimed next. The
1.5 initial proof method invoked to refine that will be offered the
1.6 facts to do ``anything appropriate'' (see also
1.7 - \secref{sec:proof-steps}). For example, method @{method_ref rule}
1.8 + \secref{sec:proof-steps}). For example, method @{method (Pure) rule}
1.9 (see \secref{sec:pure-meth-att}) would typically do an elimination
1.10 rather than an introduction. Automatic methods usually insert the
1.11 facts into the goal state before operation. This provides a simple
1.12 @@ -368,7 +368,7 @@
1.13 effect apart from entering @{text "prove(chain)"} mode, since
1.14 @{fact_ref nothing} is bound to the empty list of theorems.
1.15
1.16 - Basic proof methods (such as @{method_ref rule}) expect multiple
1.17 + Basic proof methods (such as @{method_ref (Pure) rule}) expect multiple
1.18 facts to be given in their proper order, corresponding to a prefix
1.19 of the premises of the rule involved. Note that positions may be
1.20 easily skipped using something like @{command "from"}~@{text "_
1.21 @@ -618,10 +618,11 @@
1.22 an intelligible manner.
1.23
1.24 Unless given explicitly by the user, the default initial method is
1.25 - ``@{method_ref rule}'', which applies a single standard elimination
1.26 - or introduction rule according to the topmost symbol involved.
1.27 - There is no separate default terminal method. Any remaining goals
1.28 - are always solved by assumption in the very last step.
1.29 + @{method_ref (Pure) rule} (or its classical variant @{method_ref
1.30 + rule}), which applies a single standard elimination or introduction
1.31 + rule according to the topmost symbol involved. There is no separate
1.32 + default terminal method. Any remaining goals are always solved by
1.33 + assumption in the very last step.
1.34
1.35 @{rail "
1.36 @@{command proof} method?
1.37 @@ -697,11 +698,11 @@
1.38 @{method_def "fact"} & : & @{text method} \\
1.39 @{method_def "assumption"} & : & @{text method} \\
1.40 @{method_def "this"} & : & @{text method} \\
1.41 - @{method_def "rule"} & : & @{text method} \\
1.42 + @{method_def (Pure) "rule"} & : & @{text method} \\
1.43 @{attribute_def (Pure) "intro"} & : & @{text attribute} \\
1.44 @{attribute_def (Pure) "elim"} & : & @{text attribute} \\
1.45 @{attribute_def (Pure) "dest"} & : & @{text attribute} \\
1.46 - @{attribute_def "rule"} & : & @{text attribute} \\[0.5ex]
1.47 + @{attribute_def (Pure) "rule"} & : & @{text attribute} \\[0.5ex]
1.48 @{attribute_def "OF"} & : & @{text attribute} \\
1.49 @{attribute_def "of"} & : & @{text attribute} \\
1.50 @{attribute_def "where"} & : & @{text attribute} \\
1.51 @@ -710,7 +711,7 @@
1.52 @{rail "
1.53 @@{method fact} @{syntax thmrefs}?
1.54 ;
1.55 - @@{method rule} @{syntax thmrefs}?
1.56 + @@{method (Pure) rule} @{syntax thmrefs}?
1.57 ;
1.58 rulemod: ('intro' | 'elim' | 'dest')
1.59 ((('!' | () | '?') @{syntax nat}?) | 'del') ':' @{syntax thmrefs}
1.60 @@ -718,7 +719,7 @@
1.61 (@@{attribute intro} | @@{attribute elim} | @@{attribute dest})
1.62 ('!' | () | '?') @{syntax nat}?
1.63 ;
1.64 - @@{attribute rule} 'del'
1.65 + @@{attribute (Pure) rule} 'del'
1.66 ;
1.67 @@{attribute OF} @{syntax thmrefs}
1.68 ;
1.69 @@ -734,7 +735,7 @@
1.70 \item ``@{method "-"}'' (minus) does nothing but insert the forward
1.71 chaining facts as premises into the goal. Note that command
1.72 @{command_ref "proof"} without any method actually performs a single
1.73 - reduction step using the @{method_ref rule} method; thus a plain
1.74 + reduction step using the @{method_ref (Pure) rule} method; thus a plain
1.75 \emph{do-nothing} proof step would be ``@{command "proof"}~@{text
1.76 "-"}'' rather than @{command "proof"} alone.
1.77
1.78 @@ -761,12 +762,12 @@
1.79 rules. Recall that ``@{command "."}'' (dot) abbreviates ``@{command
1.80 "by"}~@{text this}''.
1.81
1.82 - \item @{method rule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some rule given as
1.83 + \item @{method (Pure) rule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some rule given as
1.84 argument in backward manner; facts are used to reduce the rule
1.85 - before applying it to the goal. Thus @{method rule} without facts
1.86 + before applying it to the goal. Thus @{method (Pure) rule} without facts
1.87 is plain introduction, while with facts it becomes elimination.
1.88
1.89 - When no arguments are given, the @{method rule} method tries to pick
1.90 + When no arguments are given, the @{method (Pure) rule} method tries to pick
1.91 appropriate rules automatically, as declared in the current context
1.92 using the @{attribute (Pure) intro}, @{attribute (Pure) elim},
1.93 @{attribute (Pure) dest} attributes (see below). This is the
1.94 @@ -775,7 +776,7 @@
1.95
1.96 \item @{attribute (Pure) intro}, @{attribute (Pure) elim}, and
1.97 @{attribute (Pure) dest} declare introduction, elimination, and
1.98 - destruct rules, to be used with method @{method rule}, and similar
1.99 + destruct rules, to be used with method @{method (Pure) rule}, and similar
1.100 tools. Note that the latter will ignore rules declared with
1.101 ``@{text "?"}'', while ``@{text "!"}'' are used most aggressively.
1.102
1.103 @@ -784,7 +785,7 @@
1.104 present versions of Isabelle/Pure, i.e.\ @{attribute (Pure)
1.105 "Pure.intro"}.
1.106
1.107 - \item @{attribute rule}~@{text del} undeclares introduction,
1.108 + \item @{attribute (Pure) rule}~@{text del} undeclares introduction,
1.109 elimination, or destruct rules.
1.110
1.111 \item @{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some