src/HOL/Library/Inner_Product.thy
changeset 41959 b460124855b8
parent 39302 d7728f65b353
child 44126 ce44e70d0c47
     1.1 --- a/src/HOL/Library/Inner_Product.thy	Sun Mar 13 22:24:10 2011 +0100
     1.2 +++ b/src/HOL/Library/Inner_Product.thy	Sun Mar 13 22:55:50 2011 +0100
     1.3 @@ -1,5 +1,5 @@
     1.4 -(* Title:      Inner_Product.thy
     1.5 -   Author:     Brian Huffman
     1.6 +(*  Title:      HOL/Library/Inner_Product.thy
     1.7 +    Author:     Brian Huffman
     1.8  *)
     1.9  
    1.10  header {* Inner Product Spaces and the Gradient Derivative *}