src/HOL/HOL.thy
changeset 51314 eac4bb5adbf9
parent 51304 0e71a248cacb
child 51673 4dfa00e264d8
child 51687 3d8720271ebf
--- a/src/HOL/HOL.thy	Thu Feb 28 16:38:17 2013 +0100
+++ b/src/HOL/HOL.thy	Thu Feb 28 16:54:52 2013 +0100
@@ -699,8 +699,6 @@
   and [sym] = sym not_sym
   and [Pure.elim?] = iffD1 iffD2 impE
 
-ML_file "Tools/hologic.ML"
-
 
 subsubsection {* Atomizing meta-level connectives *}
 
@@ -782,6 +780,9 @@
 
 subsection {* Package setup *}
 
+ML_file "Tools/hologic.ML"
+
+
 subsubsection {* Sledgehammer setup *}
 
 text {*