| changeset 42463 | f270e3e18be5 |
| parent 41959 | b460124855b8 |
| child 44711 | cd8dbfc272df |
| 42462:0fd80c27fdf5 | 42463:f270e3e18be5 |
|---|---|
7 |
7 |
8 theory NSComplex |
8 theory NSComplex |
9 imports Complex NSA |
9 imports Complex NSA |
10 begin |
10 begin |
11 |
11 |
12 types hcomplex = "complex star" |
12 type_synonym hcomplex = "complex star" |
13 |
13 |
14 abbreviation |
14 abbreviation |
15 hcomplex_of_complex :: "complex => complex star" where |
15 hcomplex_of_complex :: "complex => complex star" where |
16 "hcomplex_of_complex == star_of" |
16 "hcomplex_of_complex == star_of" |
17 |
17 |