src/HOL/base.ML
changeset 37694 19e8b730ddeb
parent 33615 261abc2e3155
     1.1 --- a/src/HOL/base.ML	Fri Jul 02 14:23:17 2010 +0200
     1.2 +++ b/src/HOL/base.ML	Fri Jul 02 14:23:17 2010 +0200
     1.3 @@ -1,2 +1,4 @@
     1.4 -(*side-entry for HOL-Base*)
     1.5 +
     1.6 +(* side-entry for HOL-Base *)
     1.7 +
     1.8  use_thys ["HOL"];