doc-src/IsarImplementation/Thy/ML.thy
changeset 30130 e23770bc97c8
parent 29755 d66b34e46bdf
child 30270 61811c9224a6
--- a/doc-src/IsarImplementation/Thy/ML.thy	Thu Feb 26 08:44:44 2009 -0800
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Thu Feb 26 08:48:33 2009 -0800
@@ -1,6 +1,6 @@
-(* $Id$ *)
-
-theory "ML" imports base begin
+theory "ML"
+imports Base
+begin
 
 chapter {* Advanced ML programming *}