author | huffman |
Mon, 05 Jul 2010 09:12:35 -0700 | |
changeset 37731 | 8c6bfe10a4ae |
parent 37730 | 1a24950dae33 |
child 37732 | 6432bf0d7191 |
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Sun Jul 04 09:26:30 2010 -0700 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Jul 05 09:12:35 2010 -0700 @@ -3317,7 +3317,7 @@ print_antiquotations -section "Instanciate @{typ real} and @{typ complex} as typeclass @{text ordered_euclidean_space}." +subsection "Instantiate @{typ real} and @{typ complex} as typeclass @{text ordered_euclidean_space}." instantiation real :: real_basis_with_inner begin