--- a/ProgTutorial/General.thy	Fri Aug 21 11:42:14 2009 +0200
+++ b/ProgTutorial/General.thy	Fri Aug 21 16:04:59 2009 +0200
@@ -4,6 +4,14 @@
 
 chapter {* General Infrastructure *}
 
+text {*
+  Isabelle is build around a few central ideas. One is the LCF-approach to
+  theorem proving where there is a small trusted core and everything else is
+  build on top of this trusted core.
+
+*}
+
+
 section {* Terms and Types *}
 
 text {*
@@ -1642,6 +1650,16 @@
 
 ML {*Datatype.get_info @{theory} "List.list"*}
 
+text {* 
+FIXME: association lists:
+@{ML_file "Pure/General/alist.ML"}
+
+FIXME: calling the ML-compiler
+
+*}
+
+
+
 section {* Name Space Issues (TBD) *}
 
 

--- /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

--- a/ProgTutorial/Parsing.thy	Fri Aug 21 11:42:14 2009 +0200
+++ b/ProgTutorial/Parsing.thy	Fri Aug 21 16:04:59 2009 +0200
@@ -1066,6 +1066,9 @@
   
 *}
 
+
+
+
 section {* Methods (TBD) *}
 
 text {*
@@ -1110,6 +1113,10 @@
 (*<*)oops(*>*)
 
 
+
+
+
+
 (*
 ML {* SIMPLE_METHOD *}
 ML {* METHOD *}

Binary file progtutorial.pdf has changed