# HG changeset patch
# User huffman
# Date 1272558587 25200
# Node ID eacded3b05f71fa9160e013789940d68c3c351eb
# Parent  df38e0c5c12372e5130b0d87e5887670782c6dfd
remove unused function vector_power, unused lemma one_plus_of_nat_neq_0

diff -r df38e0c5c123 -r eacded3b05f7 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Apr 29 09:17:25 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Apr 29 09:29:47 2010 -0700
@@ -126,10 +126,6 @@
 instance cart :: (comm_monoid_mult,finite) comm_monoid_mult
   apply (intro_classes) by vector
 
-fun vector_power where
-  "vector_power x 0 = 1"
-  | "vector_power x (Suc n) = x * vector_power x n"
-
 instance cart :: (semiring,finite) semiring
   apply (intro_classes) by (vector field_simps)+
 
@@ -169,13 +165,6 @@
 lemma one_index[simp]:
   "(1 :: 'a::one ^'n)$i = 1" by vector
 
-lemma one_plus_of_nat_neq_0: "(1::'a::semiring_char_0) + of_nat n \<noteq> 0"
-proof-
-  have "(1::'a) + of_nat n = 0 \<longleftrightarrow> of_nat 1 + of_nat n = (of_nat 0 :: 'a)" by simp
-  also have "\<dots> \<longleftrightarrow> 1 + n = 0" by (simp only: of_nat_add[symmetric] of_nat_eq_iff)
-  finally show ?thesis by simp
-qed
-
 instance cart :: (semiring_char_0,finite) semiring_char_0
 proof (intro_classes)
   fix m n ::nat