--- a/CookBook/FirstSteps.thy	Thu Feb 19 14:44:53 2009 +0000
+++ b/CookBook/FirstSteps.thy	Fri Feb 20 23:19:41 2009 +0000
@@ -171,19 +171,11 @@
 section {* Combinators\label{sec:combinators} *}
 
 text {*
-  (FIXME: maybe move before antiquotation section)
-
   For beginners, perhaps the most puzzling parts in the existing code of Isabelle are
   the combinators. At first they seem to greatly obstruct the
   comprehension of the code, but after getting familiar with them, they
   actually ease the understanding and also the programming.
 
-  \begin{readmore}
-  The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
-  and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} 
-  contains further information about combinators.
-  \end{readmore}
-
   The simplest combinator is @{ML I}, which is just the identity function defined as
 *}
 
@@ -341,6 +333,12 @@
 text {*
   
   (FIXME: find a good exercise for combinators)
+
+  \begin{readmore}
+  The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
+  and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} 
+  contains further information about combinators.
+  \end{readmore}
  
 *}
 
@@ -874,12 +872,27 @@
   @{ML_file "Pure/thm.ML"}. 
   \end{readmore}
 
-  (FIXME: how to add case-names to goal states)
+  (FIXME: how to add case-names to goal states - maybe in the next section)
 *}
 
 
 section {* Theorem Attributes *}
 
+text {*
+  
+
+  If you want to print out all currently known attributes a theorem 
+  can have, you can use the function:
+
+  @{ML_response_fake [display,gray] "Attrib.print_attributes @{theory}" 
+"COMP:  direct composition with rules (no lifting)
+HOL.dest:  declaration of Classical destruction rule
+HOL.elim:  declaration of Classical elimination rule 
+\<dots>"}
+
+*}
+
+
 section {* Theories and Local Theories *}
 
 text {*