# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1233249013 0
# Node ID 4e3f262a459d0ac49cf1a721e458eb94fa836c7c
# Parent  667a0943c40bc059635c0af9bd06afd7a9e13723
tuned

diff -r 667a0943c40b -r 4e3f262a459d CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Thu Jan 29 17:09:56 2009 +0000
+++ b/CookBook/FirstSteps.thy	Thu Jan 29 17:10:13 2009 +0000
@@ -522,7 +522,21 @@
 
 @{ML_response [display] "Sign.base_name \"List.list.Nil\"" "\"Nil\""}
 
-  authentic syntax
+  authentic syntax?
+
+*}
+
+ML {* @{const_name lfp} *}
+
+text {*
+  constants in case-patterns?
+
+  In the meantime, lfp has been moved to the Inductive theory, so it is  
+  no longer called Lfp.lfp. If a @{text "@{const_name}"} antiquotation had been  
+  used, we would have gotten an error for this. Another advantage of the  
+  antiquotation is that we can then just write @{text "@{const_name lfp}"} rather  
+  than @{text "@{const_name Lfp.lfp}"} or whatever, and it expands to the correct  
+  name.
   
 *}
 
@@ -719,4 +733,8 @@
 thm foo_def
 (*>*)
 
+section {* Misc *}
+
+ML {*DatatypePackage.get_datatype @{theory} "List.list"*}
+
 end
\ No newline at end of file
diff -r 667a0943c40b -r 4e3f262a459d CookBook/ROOT.ML
--- a/CookBook/ROOT.ML	Thu Jan 29 17:09:56 2009 +0000
+++ b/CookBook/ROOT.ML	Thu Jan 29 17:10:13 2009 +0000
@@ -12,6 +12,7 @@
 use_thy "Package/Ind_Examples";
 use_thy "Package/Ind_General_Scheme";
 use_thy "Package/Ind_Interface";
+use_thy "Package/Ind_Code";
 
 use_thy "Appendix";
 use_thy "Recipes/NamedThms";
diff -r 667a0943c40b -r 4e3f262a459d cookbook.pdf
Binary file cookbook.pdf has changed