# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1235439015 0
# Node ID 3e94ccc0f31ed073037203a38cb572bd07dc587d
# Parent  2d9198bcb850a5cba4bfa2259dc71297f74ff8a8
polishing and start of the section about attributes

diff -r 2d9198bcb850 -r 3e94ccc0f31e CookBook/FirstSteps.thy
--- 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). 
 
diff -r 2d9198bcb850 -r 3e94ccc0f31e CookBook/Parsing.thy
--- a/CookBook/Parsing.thy	Mon Feb 23 17:08:15 2009 +0000
+++ b/CookBook/Parsing.thy	Tue Feb 24 01:30:15 2009 +0000
@@ -204,11 +204,11 @@
 *}
 
 ML{*fun p_followed_by_q p q r =
-  let 
-     val err_msg = (fn _ => p ^ " is not followed by " ^ q)
-  in
-    ($$ p -- (!! err_msg ($$ q))) || ($$ r -- $$ r)
-  end *}
+let 
+  val err_msg = (fn _ => p ^ " is not followed by " ^ q)
+in
+  ($$ p -- (!! err_msg ($$ q))) || ($$ r -- $$ r)
+end *}
 
 
 text {*
@@ -348,7 +348,7 @@
 
 text {*
   Most of the time, however, Isabelle developers have to deal with parsing
-  tokens, not strings.  These token parsers will have the type
+  tokens, not strings.  These token parsers will have the type:
 *}
   
 ML{*type 'a parser = OuterLex.token list -> 'a * OuterLex.token list*}
@@ -727,7 +727,7 @@
   The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of
   @{ML thm_name in SpecParse}. Theorem names can contain attributes. The name 
   has to end with @{text [quotes] ":"}---see the argument of 
-  @{ML SpecParse.opt_thm_name} in Line 9.
+  the function @{ML SpecParse.opt_thm_name} in Line 9.
 
   \begin{readmore}
   Attributes and arguments are implemented in the files @{ML_file "Pure/Isar/attrib.ML"} 
diff -r 2d9198bcb850 -r 3e94ccc0f31e CookBook/Tactical.thy
--- a/CookBook/Tactical.thy	Mon Feb 23 17:08:15 2009 +0000
+++ b/CookBook/Tactical.thy	Tue Feb 24 01:30:15 2009 +0000
@@ -1196,7 +1196,7 @@
 (*<*)oops(*>*)
 
 text {*
-  As usual with simplification you have to worry about looping: you already have
+  As usual with rewriting you have to worry about looping: you already have
   a loop with @{ML plus_one_sp}, if you apply it with the default simpset (because
   the default simpset contains a rule which just does the opposite of @{ML plus_one_sp},
   namely rewriting @{text [quotes] "+ 1"} to a successor). So you have to be careful 
diff -r 2d9198bcb850 -r 3e94ccc0f31e cookbook.pdf
Binary file cookbook.pdf has changed