# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1240782322 -7200
# Node ID 14d5f0cf91dc60d831cfc759fa16e3a78f0fa58b
# Parent  29d4701c5ee1b656fe690147a51d3a1916ae1734
added note about @{type_names ...}

diff -r 29d4701c5ee1 -r 14d5f0cf91dc ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Sat Apr 25 17:46:47 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sun Apr 26 23:45:22 2009 +0200
@@ -5,8 +5,7 @@
 chapter {* First Steps *}
 
 text {*
-
-  Isabelle programming is done in ML.  Just like lemmas and proofs, ML-code
+  Isabelle programming is done in ML. Just like lemmas and proofs, ML-code
   in Isabelle is part of a theory. If you want to follow the code given in
   this chapter, we assume you are working inside the theory starting with
 
@@ -890,6 +889,12 @@
   | is_nil_or_all _ = false *}
 
 text {*
+  The antiquotation for properly referencing type constants is  is @{text "@{type_name \<dots>}"}.
+  For example
+
+  @{ML_response [display,gray]
+  "@{type_name \"list\"}" "\"List.list\""}
+
   Occasionally you have to calculate what the ``base'' name of a given
   constant is. For this you can use the function @{ML Sign.extern_const} or
   @{ML Long_Name.base_name}. For example:
diff -r 29d4701c5ee1 -r 14d5f0cf91dc progtutorial.pdf
Binary file progtutorial.pdf has changed