# HG changeset patch
# User wenzelm
# Date 1210865841 -7200
# Node ID d1694ef6e7a7d321fb78cd81868b729d63a678e6
# Parent  e37358673f870c0d0cade4dfd2ceb1bf58cc12ba
fixed some Isar element markups;

diff -r e37358673f87 -r d1694ef6e7a7 doc-src/IsarRef/Thy/Generic.thy
--- a/doc-src/IsarRef/Thy/Generic.thy	Thu May 15 17:37:20 2008 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy	Thu May 15 17:37:21 2008 +0200
@@ -1325,11 +1325,11 @@
   facts, which are guaranteed to participate, may appear in either
   order.
 
-  \item [@{attribute intro} and @{attribute elim}] repeatedly refine
-  some goal by intro- or elim-resolution, after having inserted any
-  chained facts.  Exactly the rules given as arguments are taken into
-  account; this allows fine-tuned decomposition of a proof problem, in
-  contrast to common automated tools.
+  \item [@{method intro} and @{method elim}] repeatedly refine some
+  goal by intro- or elim-resolution, after having inserted any chained
+  facts.  Exactly the rules given as arguments are taken into account;
+  this allows fine-tuned decomposition of a proof problem, in contrast
+  to common automated tools.
 
   \end{descr}
 *}
diff -r e37358673f87 -r d1694ef6e7a7 doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Thu May 15 17:37:20 2008 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy	Thu May 15 17:37:21 2008 +0200
@@ -495,9 +495,9 @@
     @{method_def "this"} & : & \isarmeth \\
     @{method_def "rule"} & : & \isarmeth \\
     @{method_def "iprover"} & : & \isarmeth \\[0.5ex]
-    @{attribute_def "intro"} & : & \isaratt \\
-    @{attribute_def "elim"} & : & \isaratt \\
-    @{attribute_def "dest"} & : & \isaratt \\
+    @{attribute_def (Pure) "intro"} & : & \isaratt \\
+    @{attribute_def (Pure) "elim"} & : & \isaratt \\
+    @{attribute_def (Pure) "dest"} & : & \isaratt \\
     @{attribute_def "rule"} & : & \isaratt \\[0.5ex]
     @{attribute_def "OF"} & : & \isaratt \\
     @{attribute_def "of"} & : & \isaratt \\
@@ -565,10 +565,10 @@
   
   When no arguments are given, the @{method rule} method tries to pick
   appropriate rules automatically, as declared in the current context
-  using the @{attribute intro}, @{attribute elim}, @{attribute dest}
-  attributes (see below).  This is the default behavior of @{command
-  "proof"} and ``@{command ".."}'' (double-dot) steps (see
-  \secref{sec:proof-steps}).
+  using the @{attribute (Pure) intro}, @{attribute (Pure) elim},
+  @{attribute (Pure) dest} attributes (see below).  This is the
+  default behavior of @{command "proof"} and ``@{command ".."}'' 
+  (double-dot) steps (see \secref{sec:proof-steps}).
   
   \item [@{method iprover}] performs intuitionistic proof search,
   depending on specifically declared rules from the context, or given
@@ -576,24 +576,26 @@
   before commencing proof search; ``@{method iprover}@{text "!"}'' 
   means to include the current @{fact prems} as well.
   
-  Rules need to be classified as @{attribute intro}, @{attribute
-  elim}, or @{attribute dest}; here the ``@{text "!"}'' indicator
-  refers to ``safe'' rules, which may be applied aggressively (without
-  considering back-tracking later).  Rules declared with ``@{text
-  "?"}'' are ignored in proof search (the single-step @{method rule}
-  method still observes these).  An explicit weight annotation may be
-  given as well; otherwise the number of rule premises will be taken
-  into account here.
+  Rules need to be classified as @{attribute (Pure) intro},
+  @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
+  ``@{text "!"}'' indicator refers to ``safe'' rules, which may be
+  applied aggressively (without considering back-tracking later).
+  Rules declared with ``@{text "?"}'' are ignored in proof search (the
+  single-step @{method rule} method still observes these).  An
+  explicit weight annotation may be given as well; otherwise the
+  number of rule premises will be taken into account here.
   
-  \item [@{attribute intro}, @{attribute elim}, and @{attribute dest}]
-  declare introduction, elimination, and destruct rules, to be used
-  with the @{method rule} and @{method iprover} methods.  Note that
-  the latter will ignore rules declared with ``@{text "?"}'', while
-  ``@{text "!"}''  are used most aggressively.
+  \item [@{attribute (Pure) intro}, @{attribute (Pure) elim}, and
+  @{attribute (Pure) dest}] declare introduction, elimination, and
+  destruct rules, to be used with the @{method rule} and @{method
+  iprover} methods.  Note that the latter will ignore rules declared
+  with ``@{text "?"}'', while ``@{text "!"}''  are used most
+  aggressively.
   
   The classical reasoner (see \secref{sec:classical}) introduces its
   own variants of these attributes; use qualified names to access the
-  present versions of Isabelle/Pure, i.e.\ @{attribute "Pure.intro"}.
+  present versions of Isabelle/Pure, i.e.\ @{attribute (Pure)
+  "Pure.intro"}.
   
   \item [@{attribute rule}~@{text del}] undeclares introduction,
   elimination, or destruct rules.