src/HOL/Multivariate_Analysis/Euclidean_Space.thy
changeset 37731 8c6bfe10a4ae
parent 37664 2946b8f057df
child 37737 243ea7885e05
equal deleted inserted replaced
37730:1a24950dae33 37731:8c6bfe10a4ae
  3315 apply simp
  3315 apply simp
  3316 done
  3316 done
  3317 
  3317 
  3318 print_antiquotations
  3318 print_antiquotations
  3319 
  3319 
  3320 section "Instanciate @{typ real} and @{typ complex} as typeclass @{text ordered_euclidean_space}."
  3320 subsection "Instantiate @{typ real} and @{typ complex} as typeclass @{text ordered_euclidean_space}."
  3321 
  3321 
  3322 instantiation real :: real_basis_with_inner
  3322 instantiation real :: real_basis_with_inner
  3323 begin
  3323 begin
  3324 definition [simp]: "basis i = (if i = 0 then (1::real) else 0)"
  3324 definition [simp]: "basis i = (if i = 0 then (1::real) else 0)"
  3325 
  3325