src/HOL/Library/Euclidean_Space.thy
changeset 29906 80369da39838
parent 29905 26ee9656872a
child 30039 7208c88df507
child 30240 5b25fee0362c
     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Fri Feb 13 14:41:54 2009 -0800
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Fri Feb 13 14:45:10 2009 -0800
     1.3 @@ -40,7 +40,7 @@
     1.4  lemma setsum_3: "setsum f {1::nat..3} = f 1 + f 2 + f 3" 
     1.5    by (simp add: nat_number  atLeastAtMostSuc_conv add_commute)
     1.6  
     1.7 -section{* Basic componentwise operations on vectors. *}
     1.8 +subsection{* Basic componentwise operations on vectors. *}
     1.9  
    1.10  instantiation "^" :: (plus,type) plus
    1.11  begin
    1.12 @@ -106,7 +106,7 @@
    1.13  lemma dot_3[simp]: "(x::'a::{comm_monoid_add, times}^3) \<bullet> y = (x$1) * (y$1) + (x$2) * (y$2) + (x$3) * (y$3)"
    1.14    by (simp add: dot_def dimindex_def nat_number)
    1.15  
    1.16 -section {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *}
    1.17 +subsection {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *}
    1.18  
    1.19  lemmas Cart_lambda_beta' = Cart_lambda_beta[rule_format]
    1.20  method_setup vector = {*