src/HOL/HOL.ML
changeset 5809 bacf85370ce0
parent 5760 7e2cf2820684
child 5888 d8e51792ca85
     1.1 --- a/src/HOL/HOL.ML	Fri Nov 06 15:48:37 1998 +0100
     1.2 +++ b/src/HOL/HOL.ML	Mon Nov 09 10:58:49 1998 +0100
     1.3 @@ -3,12 +3,9 @@
     1.4      Author:     Tobias Nipkow
     1.5      Copyright   1991  University of Cambridge
     1.6  
     1.7 -For HOL.thy
     1.8  Derived rules from Appendix of Mike Gordons HOL Report, Cambridge TR 68 
     1.9  *)
    1.10  
    1.11 -open HOL;
    1.12 -
    1.13  
    1.14  (** Equality **)
    1.15  section "=";