src/HOL/Metis.thy
changeset 54148 c8cc5ab4a863
parent 52641 c56b6fa636e8
child 55178 318cd8ac1817
     1.1 --- a/src/HOL/Metis.thy	Fri Oct 18 10:43:20 2013 +0200
     1.2 +++ b/src/HOL/Metis.thy	Fri Oct 18 10:43:21 2013 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4  subsection {* Literal selection and lambda-lifting helpers *}
     1.5  
     1.6  definition select :: "'a \<Rightarrow> 'a" where
     1.7 -[no_atp]: "select = (\<lambda>x. x)"
     1.8 +"select = (\<lambda>x. x)"
     1.9  
    1.10  lemma not_atomize: "(\<not> A \<Longrightarrow> False) \<equiv> Trueprop A"
    1.11  by (cut_tac atomize_not [of "\<not> A"]) simp
    1.12 @@ -30,7 +30,7 @@
    1.13  lemma select_FalseI: "False \<Longrightarrow> select False" by simp
    1.14  
    1.15  definition lambda :: "'a \<Rightarrow> 'a" where
    1.16 -[no_atp]: "lambda = (\<lambda>x. x)"
    1.17 +"lambda = (\<lambda>x. x)"
    1.18  
    1.19  lemma eq_lambdaI: "x \<equiv> y \<Longrightarrow> x \<equiv> lambda y"
    1.20  unfolding lambda_def by assumption