--- a/src/HOL/Imperative_HOL/Array.thy Fri Feb 06 08:23:15 2009 +0000
+++ b/src/HOL/Imperative_HOL/Array.thy Fri Feb 06 15:15:27 2009 +0100
@@ -32,15 +32,6 @@
else raise (''array lookup: index out of range''))
done)"
--- {* FIXME adjustion for List theory *}
-no_syntax
- nth :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!" 100)
-
-abbreviation
- nth_list :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!" 100)
-where
- "nth_list \<equiv> List.nth"
-
definition
upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap"
where
--- a/src/HOL/Imperative_HOL/Imperative_HOL.thy Fri Feb 06 08:23:15 2009 +0000
+++ b/src/HOL/Imperative_HOL/Imperative_HOL.thy Fri Feb 06 15:15:27 2009 +0100
@@ -1,5 +1,4 @@
-(* Title: HOL/Library/Imperative_HOL.thy
- ID: $Id$
+(* Title: HOL/Imperative_HOL/Imperative_HOL.thy
Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
*)
--- a/src/HOL/List.thy Fri Feb 06 08:23:15 2009 +0000
+++ b/src/HOL/List.thy Fri Feb 06 15:15:27 2009 +0100
@@ -27,7 +27,6 @@
set :: "'a list => 'a set"
map :: "('a=>'b) => ('a list => 'b list)"
listsum :: "'a list => 'a::monoid_add"
- nth :: "'a list => nat => 'a" (infixl "!" 100)
list_update :: "'a list => nat => 'a => 'a list"
take:: "nat => 'a list => 'a list"
drop:: "nat => 'a list => 'a list"
@@ -146,8 +145,8 @@
-- {*Warning: simpset does not contain this definition, but separate
theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
-primrec
- nth_Cons:"(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)"
+primrec nth :: "'a list => nat => 'a" (infixl "!" 100) where
+ nth_Cons: "(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)"
-- {*Warning: simpset does not contain this definition, but separate
theorems for @{text "n = 0"} and @{text "n = Suc k"} *}