*** empty log message ***
authornipkow
Fri Jul 21 12:30:08 2000 +0200 (2000-07-21)
changeset 9396a1b31d61f8e1
parent 9395 1c9851cdfe9f
child 9397 358e67410253
*** empty log message ***
src/HOL/HOL.ML
     1.1 --- a/src/HOL/HOL.ML	Fri Jul 21 10:28:32 2000 +0200
     1.2 +++ b/src/HOL/HOL.ML	Fri Jul 21 12:30:08 2000 +0200
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  structure HOL =
     1.6  struct
     1.7    val thy = the_context ();