# HG changeset patch
# User haftmann
# Date 1233929727 -3600
# Node ID c45845743f041c45e54e300075cb25458f6dc1ed
# Parent  7e4161257c9a52dde1337f7f437843724054e979
authentic syntax for List.nth

diff -r 7e4161257c9a -r c45845743f04 src/HOL/Imperative_HOL/Array.thy
--- 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
diff -r 7e4161257c9a -r c45845743f04 src/HOL/Imperative_HOL/Imperative_HOL.thy
--- 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
 *)
 
diff -r 7e4161257c9a -r c45845743f04 src/HOL/List.thy
--- 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"} *}