doc-src/IsarImplementation/Thy/ML.thy

--- a/doc-src/IsarImplementation/Thy/ML.thy	Mon Jan 02 20:16:52 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Mon Jan 02 20:42:12 2006 +0100
@@ -1,2 +1,15 @@
 
-theory "ML" imports Pure begin end
+(* $Id$ *)
+
+theory "ML" imports base begin
+
+chapter {* Aesthetics of ML programming *}
+
+text {* FIXME style guide *}
+
+
+chapter {* Basic library functions *}
+
+text {* FIXME beyond the basis library definition *}
+
+end