equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*} |
6 header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*} |
7 |
7 |
8 theory NSA |
8 theory NSA |
9 imports HyperDef |
9 imports HyperDef "~~/src/HOL/Library/Lubs_Glbs" |
10 begin |
10 begin |
11 |
11 |
12 definition |
12 definition |
13 hnorm :: "'a::real_normed_vector star \<Rightarrow> real star" where |
13 hnorm :: "'a::real_normed_vector star \<Rightarrow> real star" where |
14 [transfer_unfold]: "hnorm = *f* norm" |
14 [transfer_unfold]: "hnorm = *f* norm" |