equal
deleted
inserted
replaced
3313 apply (simp add: field_simps) |
3313 apply (simp add: field_simps) |
3314 apply simp |
3314 apply simp |
3315 apply simp |
3315 apply simp |
3316 done |
3316 done |
3317 |
3317 |
3318 print_antiquotations |
|
3319 |
|
3320 subsection "Instantiate @{typ real} and @{typ complex} as typeclass @{text ordered_euclidean_space}." |
3318 subsection "Instantiate @{typ real} and @{typ complex} as typeclass @{text ordered_euclidean_space}." |
3321 |
3319 |
3322 instantiation real :: real_basis_with_inner |
3320 instantiation real :: real_basis_with_inner |
3323 begin |
3321 begin |
3324 definition [simp]: "basis i = (if i = 0 then (1::real) else 0)" |
3322 definition [simp]: "basis i = (if i = 0 then (1::real) else 0)" |