# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1235483834 0
# Node ID 58277de8493cae7dced3f3aff1d006a39bb7192a
# Parent  8c31b729a5df436705b7b91de8d8934f3d5ad647
to be in sync with Sascha

diff -r 8c31b729a5df -r 58277de8493c CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Tue Feb 24 14:35:07 2009 +0100
+++ b/CookBook/FirstSteps.thy	Tue Feb 24 13:57:14 2009 +0000
@@ -890,10 +890,10 @@
 
 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
+  "[symmetric]"} and so on. Such attributes are \emph{neither} tags \emph{nor} flags
+  annotated to theorems, but functions that do further processing once a
+  theorem is proven. In particular, it is not possible to find out
+  what are all theorems that have a 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}. 
@@ -907,12 +907,23 @@
 HOL.elim:  declaration of Classical elimination rule 
 \<dots>"}
 
+  To explain how to write your own attribute, let us start with an extremely simple 
+  version of the attribute @{text "[symmetric]"}. The purpose of this attribute is
+  to produce the ``symmetric'' version of an equation. The main function behind 
+  this attribute is
 *}
 
 ML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*}
 
 text {* 
-  the setup
+  where the function @{ML "Thm.rule_attribute"} expects a function taking a 
+  context (we ignore it in the code above) and a theorem (@{text thm}) and 
+  returns another theorem (namely @{text thm} resolved with the rule 
+  @{thm sym[no_vars]}). The function @{ML "Thm.rule_attribute"} then returns 
+  an attribute (of type @{ML_type "attribute"}).
+
+  Before we can use the attribute, we need to set it up. This can be done
+  using the function @{ML Attrib.add_attributes} as follows.
 *}
 
 setup {*
@@ -920,16 +931,29 @@
     [("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")]
 *}
 
-lemma test: "1 = Suc 0" by simp
+text {*
+  The attribute does not expect any further arguments (like @{text "[OF \<dots>]"} that 
+  can take a list of theorems as argument). Therefore we use the function
+  @{ML Attrib.no_args}. Later on we will also consider attributes taking further
+  arguments. An example for the attribute @{text "[my_sym]"} is the proof
+*} 
+
+lemma test[my_sym]: "2 = Suc (Suc 0)" by simp
 
 text {*
-  @{thm test[my_sym]}
+  which stores the theorem @{thm test} under the name @{thm [source] test}. We 
+  can also use the attribute when referring to this theorem.
+
+  \begin{isabelle}
+  \isacommand{thm}~@{text "test[my_sym]"}\\
+  @{text "> "}~@{thm test[my_sym]}
+  \end{isabelle}
+
 *}
 
 text {*
 What are: 
 
-@{text "rule_attribute"}
 
 @{text "declaration_attribute"}
 
diff -r 8c31b729a5df -r 58277de8493c cookbook.pdf
Binary file cookbook.pdf has changed