src/HOL/HOL.thy
changeset 51314 eac4bb5adbf9
parent 51304 0e71a248cacb
child 51673 4dfa00e264d8
child 51687 3d8720271ebf
     1.1 --- a/src/HOL/HOL.thy	Thu Feb 28 16:38:17 2013 +0100
     1.2 +++ b/src/HOL/HOL.thy	Thu Feb 28 16:54:52 2013 +0100
     1.3 @@ -699,8 +699,6 @@
     1.4    and [sym] = sym not_sym
     1.5    and [Pure.elim?] = iffD1 iffD2 impE
     1.6  
     1.7 -ML_file "Tools/hologic.ML"
     1.8 -
     1.9  
    1.10  subsubsection {* Atomizing meta-level connectives *}
    1.11  
    1.12 @@ -782,6 +780,9 @@
    1.13  
    1.14  subsection {* Package setup *}
    1.15  
    1.16 +ML_file "Tools/hologic.ML"
    1.17 +
    1.18 +
    1.19  subsubsection {* Sledgehammer setup *}
    1.20  
    1.21  text {*