src/HOL/plain.ML
changeset 37694 19e8b730ddeb
parent 33615 261abc2e3155
--- a/src/HOL/plain.ML	Fri Jul 02 14:23:17 2010 +0200
+++ b/src/HOL/plain.ML	Fri Jul 02 14:23:17 2010 +0200
@@ -1,2 +1,4 @@
-(*side-entry for HOL-Plain*)
+
+(* side-entry for HOL-Plain *)
+
 use_thys ["Plain"];