diff -r 97a8ff4e4ac9 -r c8cc5ab4a863 src/HOL/ATP.thy
--- a/src/HOL/ATP.thy	Fri Oct 18 10:43:20 2013 +0200
+++ b/src/HOL/ATP.thy	Fri Oct 18 10:43:21 2013 +0200
@@ -18,34 +18,34 @@
 
 subsection {* Higher-order reasoning helpers *}
 
-definition fFalse :: bool where [no_atp]:
+definition fFalse :: bool where
 "fFalse \<longleftrightarrow> False"
 
-definition fTrue :: bool where [no_atp]:
+definition fTrue :: bool where
 "fTrue \<longleftrightarrow> True"
 
-definition fNot :: "bool \<Rightarrow> bool" where [no_atp]:
+definition fNot :: "bool \<Rightarrow> bool" where
 "fNot P \<longleftrightarrow> \<not> P"
 
-definition fComp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
+definition fComp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
 "fComp P = (\<lambda>x. \<not> P x)"
 
-definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
+definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
 "fconj P Q \<longleftrightarrow> P \<and> Q"
 
-definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
+definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
 "fdisj P Q \<longleftrightarrow> P \<or> Q"
 
-definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
+definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
 "fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
 
-definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
+definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
 "fequal x y \<longleftrightarrow> (x = y)"
 
-definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
+definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
 "fAll P \<longleftrightarrow> All P"
 
-definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
+definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
 "fEx P \<longleftrightarrow> Ex P"
 
 lemma fTrue_ne_fFalse: "fFalse \<noteq> fTrue"