src/HOL/Imperative_HOL/Array.thy
changeset 29822 c45845743f04
parent 29815 9e94b7078fa5
child 31203 5c8fb4fd67e0
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Fri Feb 06 08:23:15 2009 +0000
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Fri Feb 06 15:15:27 2009 +0100
     1.3 @@ -32,15 +32,6 @@
     1.4                       else raise (''array lookup: index out of range''))
     1.5                done)"
     1.6  
     1.7 --- {* FIXME adjustion for List theory *}
     1.8 -no_syntax
     1.9 -  nth  :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!" 100)
    1.10 -
    1.11 -abbreviation
    1.12 -  nth_list :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!" 100)
    1.13 -where
    1.14 -  "nth_list \<equiv> List.nth"
    1.15 -
    1.16  definition
    1.17    upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap"
    1.18  where