--- 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) *}