| changeset 25502 | 9200b36280c0 |
| parent 25335 | 182a001a7ea4 |
| child 25691 | 8f8d83af100a |
--- a/src/HOL/Library/Code_Index.thy Thu Nov 29 07:55:46 2007 +0100 +++ b/src/HOL/Library/Code_Index.thy Thu Nov 29 17:08:26 2007 +0100 @@ -143,7 +143,7 @@ by simp instance index :: abs - "\<bar>k\<bar> \<equiv> if k < 0 then -k else k" .. + "\<bar>k\<Colon>index\<bar> \<equiv> if k < 0 then -k else k" .. lemma index_of_int [code func]: "index_of_int k = (if k = 0 then 0