equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*} |
8 header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*} |
9 |
9 |
10 theory NSA |
10 theory NSA |
11 imports HyperDef "../Real/RComplete" |
11 imports HyperDef RComplete |
12 begin |
12 begin |
13 |
13 |
14 definition |
14 definition |
15 hnorm :: "'a::norm star \<Rightarrow> real star" where |
15 hnorm :: "'a::norm star \<Rightarrow> real star" where |
16 [transfer_unfold]: "hnorm = *f* norm" |
16 [transfer_unfold]: "hnorm = *f* norm" |