src/HOL/Plain.thy

--- a/src/HOL/Plain.thy	Thu Jan 01 23:31:59 2009 +0100
+++ b/src/HOL/Plain.thy	Fri Jan 02 00:21:59 2009 +0100
@@ -1,15 +1,14 @@
-(*  Title:      HOL/Plain.thy
-    ID:         $Id$
-
-Contains fundamental HOL tools and packages.  Does not include Hilbert_Choice.
-*)
-
 header {* Plain HOL *}
 
 theory Plain
 imports Datatype FunDef Record SAT Extraction
 begin
 
+text {*
+  Plain bootstrap of fundamental HOL tools and packages; does not
+  include @{text Hilbert_Choice}.
+*}
+
 ML {* path_add "~~/src/HOL/Library" *}
 
 end