| changeset 42463 | f270e3e18be5 |
| parent 37765 | 26bdfb7b680b |
| child 57512 | cc97b347b301 |
| 42462:0fd80c27fdf5 | 42463:f270e3e18be5 |
|---|---|
9 |
9 |
10 theory HyperNat |
10 theory HyperNat |
11 imports StarDef |
11 imports StarDef |
12 begin |
12 begin |
13 |
13 |
14 types hypnat = "nat star" |
14 type_synonym hypnat = "nat star" |
15 |
15 |
16 abbreviation |
16 abbreviation |
17 hypnat_of_nat :: "nat => nat star" where |
17 hypnat_of_nat :: "nat => nat star" where |
18 "hypnat_of_nat == star_of" |
18 "hypnat_of_nat == star_of" |
19 |
19 |