--- a/ProgTutorial/Package/Ind_Extensions.thy	Sat May 09 18:50:01 2009 +0200
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Sun May 17 16:22:27 2009 +0200
@@ -188,6 +188,12 @@
   \end{readmore}
 *}
 
+section {* Definitional Packages *}
+
+text {* Type declarations *}
+
+ML{*TypedefPackage.add_typedef false NONE (@{binding test},[],NoSyn)
+  @{term "{1}::nat set"} NONE (simp_tac @{simpset} 1) @{theory} *}
 
 
 (*<*)end(*>*)
\ No newline at end of file