--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/Helper/Command/Command.thy	Fri Aug 21 16:04:59 2009 +0200
@@ -0,0 +1,22 @@
+theory Command
+imports Main
+begin
+ML {*
+let
+   val do_nothing = Scan.succeed (LocalTheory.theory I)
+   val kind = OuterKeyword.thy_goal
+in
+   OuterSyntax.local_theory "foobar" "description of foobar" kind do_nothing
+end
+*}
+
+ML {*
+let
+   val do_nothing = Scan.succeed (LocalTheory.theory I)
+   val kind = OuterKeyword.thy_decl
+in
+   OuterSyntax.local_theory "simple_induct" "description of foobar" kind do_nothing
+end
+*}
+
+end