# HG changeset patch
# User wenzelm
# Date 1136230932 -3600
# Node ID 88fe84d4d151b19d8ff70a7d07b777a95dc27667
# Parent  2681f9e343903e6ff1de21e9ca36f54f3a3e82d3
outline;

diff -r 2681f9e34390 -r 88fe84d4d151 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