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 {*