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