138   unfolding permute_flip_at by simp_all

   138   unfolding permute_flip_at by simp_all

   139 

   139 

   140 

   140 

   141 subsection {* Syntax for coercing at-elements to the atom-type *}

   141 subsection {* Syntax for coercing at-elements to the atom-type *}

   142 

   142 

   143 syntax

   144 syntax

   144   "_atom_constrain" :: "logic \<Rightarrow> type \<Rightarrow> logic" ("_:::_" [4, 0] 3)

   145   "_atom_constrain" :: "logic \<Rightarrow> type \<Rightarrow> logic" ("_:::_" [4, 0] 3)

   145 

   146 

   146 translations

   147 translations

   147   "_atom_constrain a t" => "atom (_constrain a t)"

   148   "_atom_constrain a t" => "atom (_constrain a t)"

   149 

   150 

   150 subsection {* A lemma for proving instances of class @{text at}. *}

   151 subsection {* A lemma for proving instances of class @{text at}. *}

   151 

   152 

   152 setup {* Sign.add_const_constraint (@{const_name "permute"}, NONE) *}

   153 setup {* Sign.add_const_constraint (@{const_name "permute"}, NONE) *}

   153 setup {* Sign.add_const_constraint (@{const_name "atom"}, NONE) *}

   154 setup {* Sign.add_const_constraint (@{const_name "atom"}, NONE) *}