equal
deleted
inserted
replaced
28 |
28 |
29 text{* There are numerous facts that come with this declaration: for example that |
29 text{* There are numerous facts that come with this declaration: for example that |
30 there are infinitely many elements in @{text "tyvrs"} and @{text "vrs"}. *} |
30 there are infinitely many elements in @{text "tyvrs"} and @{text "vrs"}. *} |
31 |
31 |
32 text{* The constructors for types and terms in System \FSUB{} contain abstractions |
32 text{* The constructors for types and terms in System \FSUB{} contain abstractions |
33 over type-variables and term-variables. The nominal datatype-package uses |
33 over type-variables and term-variables. The nominal datatype package uses |
34 @{text "\<guillemotleft>\<dots>\<guillemotright>\<dots>"} to indicate where abstractions occur. *} |
34 @{text "\<guillemotleft>\<dots>\<guillemotright>\<dots>"} to indicate where abstractions occur. *} |
35 |
35 |
36 nominal_datatype ty = |
36 nominal_datatype ty = |
37 Tvar "tyvrs" |
37 Tvar "tyvrs" |
38 | Top |
38 | Top |