src/HOL/ATP.thy
changeset 54148 c8cc5ab4a863
parent 53479 f7d8224641de
child 56946 10d9bd4ea94f
     1.1 --- a/src/HOL/ATP.thy	Fri Oct 18 10:43:20 2013 +0200
     1.2 +++ b/src/HOL/ATP.thy	Fri Oct 18 10:43:21 2013 +0200
     1.3 @@ -18,34 +18,34 @@
     1.4  
     1.5  subsection {* Higher-order reasoning helpers *}
     1.6  
     1.7 -definition fFalse :: bool where [no_atp]:
     1.8 +definition fFalse :: bool where
     1.9  "fFalse \<longleftrightarrow> False"
    1.10  
    1.11 -definition fTrue :: bool where [no_atp]:
    1.12 +definition fTrue :: bool where
    1.13  "fTrue \<longleftrightarrow> True"
    1.14  
    1.15 -definition fNot :: "bool \<Rightarrow> bool" where [no_atp]:
    1.16 +definition fNot :: "bool \<Rightarrow> bool" where
    1.17  "fNot P \<longleftrightarrow> \<not> P"
    1.18  
    1.19 -definition fComp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
    1.20 +definition fComp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
    1.21  "fComp P = (\<lambda>x. \<not> P x)"
    1.22  
    1.23 -definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
    1.24 +definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
    1.25  "fconj P Q \<longleftrightarrow> P \<and> Q"
    1.26  
    1.27 -definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
    1.28 +definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
    1.29  "fdisj P Q \<longleftrightarrow> P \<or> Q"
    1.30  
    1.31 -definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
    1.32 +definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
    1.33  "fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
    1.34  
    1.35 -definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
    1.36 +definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
    1.37  "fequal x y \<longleftrightarrow> (x = y)"
    1.38  
    1.39 -definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
    1.40 +definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
    1.41  "fAll P \<longleftrightarrow> All P"
    1.42  
    1.43 -definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
    1.44 +definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
    1.45  "fEx P \<longleftrightarrow> Ex P"
    1.46  
    1.47  lemma fTrue_ne_fFalse: "fFalse \<noteq> fTrue"