--- a/src/HOL/ATP.thy Mon Jun 16 13:19:48 2014 +0200
+++ b/src/HOL/ATP.thy Mon Jun 16 16:18:15 2014 +0200
@@ -16,7 +16,6 @@
ML_file "Tools/ATP/atp_proof.ML"
ML_file "Tools/ATP/atp_proof_redirect.ML"
-
subsection {* Higher-order reasoning helpers *}
definition fFalse :: bool where