--- a/CookBook/FirstSteps.thy	Mon Feb 23 17:08:15 2009 +0000
+++ b/CookBook/FirstSteps.thy	Tue Feb 24 01:30:15 2009 +0000
@@ -377,11 +377,11 @@
   replaced with the value representing the theory name.
 
   In a similar way you can use antiquotations to refer to proved theorems: 
-  for a single theorem
+  @{text "@{thm \<dots>}"} for a single theorem
 
   @{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
 
-  and for more than one
+  and @{text "@{thms \<dots>}"} for more than one
 
 @{ML_response_fake [display,gray] "@{thms conj_ac}" 
 "(?P \<and> ?Q) = (?Q \<and> ?P)
@@ -885,11 +885,17 @@
   (FIXME: how to add case-names to goal states - maybe in the next section)
 *}
 
-
 section {* Theorem Attributes *}
 
 text {*
-  
+  Theorem attributes are @{text "[simp]"}, @{text "[OF \<dots>]"}, @{text
+  "[symmetric]"} and so on. Such attributes are \emph{neither} tags \emph{or} flags
+  annotated to theorems, but functions that do further processing once the
+  theorems are proven. In particular, it is not possible to find out
+  what are all theorems that have an given attribute in common, unless of course
+  the function behind the attribute stores the theorems in a retrivable 
+  datastructure. This can be easily done by the recipe described in 
+  \ref{rec:named}. 
 
   If you want to print out all currently known attributes a theorem 
   can have, you can use the function:
@@ -902,12 +908,50 @@
 
 *}
 
+ML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*}
+
+text {* 
+  the setup
+*}
+
+setup {*
+  Attrib.add_attributes 
+    [("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")]
+*}
+
+lemma test: "1 = Suc 0" by simp
+
+text {*
+  @{thm test[my_sym]}
+*}
+
+text {*
+What are: 
+
+@{text "rule_attribute"}
+
+@{text "declaration_attribute"}
+
+@{text "theory_attributes"}
+
+@{text "proof_attributes"}
+
+
+  \begin{readmore}
+  FIXME: @{ML_file "Pure/more_thm.ML"} @{ML_file "Pure/Isar/attrib.ML"}
+  \end{readmore}
+
+
+*}
+
 
 section {* Theories and Local Theories *}
 
 text {*
   (FIXME: expand)
 
+  (FIXME: explain \isacommand{setup})
+
   There are theories, proof contexts and local theories (in this order, if you
   want to order them).