| changeset 22473 | 753123c89d72 |
| parent 22333 | 652f316ca26a |
| 22472:bfd9c0fd70b1 | 22473:753123c89d72 |
|---|---|
8 imports CodeEmbed |
8 imports CodeEmbed |
9 begin |
9 begin |
10 |
10 |
11 subsection {* The typ_of class *} |
11 subsection {* The typ_of class *} |
12 |
12 |
13 class typ_of = |
13 class typ_of = type + |
14 fixes typ_of :: "'a itself \<Rightarrow> typ" |
14 fixes typ_of :: "'a itself \<Rightarrow> typ" |
15 |
15 |
16 ML {* |
16 ML {* |
17 structure TypOf = |
17 structure TypOf = |
18 struct |
18 struct |