src/HOL/List.thy
changeset 36176 3fe7e97ccca8
parent 36154 11c6106d7787
child 36199 4d220994f30b
equal deleted inserted replaced
36175:5cec4ca719d1 36176:3fe7e97ccca8
   170 
   170 
   171 definition
   171 definition
   172   insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   172   insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   173   "insert x xs = (if x \<in> set xs then xs else x # xs)"
   173   "insert x xs = (if x \<in> set xs then xs else x # xs)"
   174 
   174 
   175 hide (open) const insert hide (open) fact insert_def
   175 hide_const (open) insert
       
   176 hide_fact (open) insert_def
   176 
   177 
   177 primrec
   178 primrec
   178   remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   179   remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   179     "remove1 x [] = []"
   180     "remove1 x [] = []"
   180   | "remove1 x (y # xs) = (if x = y then xs else y # remove1 x xs)"
   181   | "remove1 x (y # xs) = (if x = y then xs else y # remove1 x xs)"
  4582 declare INFI_def [code_unfold]
  4583 declare INFI_def [code_unfold]
  4583 declare SUPR_def [code_unfold]
  4584 declare SUPR_def [code_unfold]
  4584 
  4585 
  4585 declare set_map [symmetric, code_unfold]
  4586 declare set_map [symmetric, code_unfold]
  4586 
  4587 
  4587 hide (open) const length_unique
  4588 hide_const (open) length_unique
  4588 
  4589 
  4589 
  4590 
  4590 text {* Code for bounded quantification and summation over nats. *}
  4591 text {* Code for bounded quantification and summation over nats. *}
  4591 
  4592 
  4592 lemma atMost_upto [code_unfold]:
  4593 lemma atMost_upto [code_unfold]: