# HG changeset patch
# User haftmann
# Date 1213104661 -7200
# Node ID 779e73b02ccad7a214358dacd1b7118d978e5ff0
# Parent  e447b31076968f760aaeb43747b230586c232d21
more instantiation

diff -r e447b3107696 -r 779e73b02cca src/HOL/Library/ListVector.thy
--- a/src/HOL/Library/ListVector.thy	Tue Jun 10 15:30:59 2008 +0200
+++ b/src/HOL/Library/ListVector.thy	Tue Jun 10 15:31:01 2008 +0200
@@ -29,19 +29,39 @@
 "zipwith0 f (x#xs) [] = f x 0 # zipwith0 f xs []" |
 "zipwith0 f [] (y#ys) = f 0 y # zipwith0 f [] ys"
 
-instance list :: ("{zero,plus}")plus
-list_add_def : "op + \<equiv> zipwith0 (op +)" ..
+instantiation list :: ("{zero, plus}") plus
+begin
+
+definition
+  list_add_def: "op + = zipwith0 (op +)"
+
+instance ..
+
+end
+
+instantiation list :: ("{zero, uminus}") uminus
+begin
 
-instance list :: ("{zero,uminus}")uminus
-list_uminus_def: "uminus \<equiv> map uminus" ..
+definition
+  list_uminus_def: "uminus = map uminus"
+
+instance ..
+
+end
 
-instance list :: ("{zero,minus}")minus
-list_diff_def: "op - \<equiv> zipwith0 (op -)" ..
+instantiation list :: ("{zero,minus}") minus
+begin
+
+definition
+  list_diff_def: "op - = zipwith0 (op -)"
+
+instance ..
+
+end
 
 lemma zipwith0_Nil[simp]: "zipwith0 f [] ys = map (f 0) ys"
 by(induct ys) simp_all
 
-
 lemma list_add_Nil[simp]: "[] + xs = (xs::'a::monoid_add list)"
 by (induct xs) (auto simp:list_add_def)