ProgTutorial/General.thy
changeset 319 6bce4acf7f2a
parent 318 efb5fff99c96
child 323 92f6a772e013
--- 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) *}