src/HOL/List.thy
changeset 41229 d797baa3d57c
parent 41075 4bed56dc95fb
child 41372 551eb49a6e91
equal deleted inserted replaced
41228:e1fce873b814 41229:d797baa3d57c
   121 primrec
   121 primrec
   122   list_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
   122   list_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
   123     "list_update [] i v = []"
   123     "list_update [] i v = []"
   124   | "list_update (x # xs) i v = (case i of 0 \<Rightarrow> v # xs | Suc j \<Rightarrow> x # list_update xs j v)"
   124   | "list_update (x # xs) i v = (case i of 0 \<Rightarrow> v # xs | Suc j \<Rightarrow> x # list_update xs j v)"
   125 
   125 
   126 nonterminals lupdbinds lupdbind
   126 nonterminal lupdbinds and lupdbind
   127 
   127 
   128 syntax
   128 syntax
   129   "_lupdbind":: "['a, 'a] => lupdbind"    ("(2_ :=/ _)")
   129   "_lupdbind":: "['a, 'a] => lupdbind"    ("(2_ :=/ _)")
   130   "" :: "lupdbind => lupdbinds"    ("_")
   130   "" :: "lupdbind => lupdbinds"    ("_")
   131   "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds"    ("_,/ _")
   131   "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds"    ("_,/ _")
   344 @{text"set[f x y. x \<leftarrow> xs, y \<leftarrow> ys, P x y]"}
   344 @{text"set[f x y. x \<leftarrow> xs, y \<leftarrow> ys, P x y]"}
   345 produced something like
   345 produced something like
   346 @{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}.
   346 @{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}.
   347 *)
   347 *)
   348 
   348 
   349 nonterminals lc_qual lc_quals
   349 nonterminal lc_qual and lc_quals
   350 
   350 
   351 syntax
   351 syntax
   352 "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  ("[_ . __")
   352 "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  ("[_ . __")
   353 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _")
   353 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _")
   354 "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
   354 "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")