# 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