equal
deleted
inserted
replaced
3 Nominal2_Base Nominal2_Eqvt Nominal2_Abs |
3 Nominal2_Base Nominal2_Eqvt Nominal2_Abs |
4 uses ("nominal_dt_rawperm.ML") |
4 uses ("nominal_dt_rawperm.ML") |
5 ("nominal_dt_rawfuns.ML") |
5 ("nominal_dt_rawfuns.ML") |
6 ("nominal_dt_alpha.ML") |
6 ("nominal_dt_alpha.ML") |
7 ("nominal_dt_quot.ML") |
7 ("nominal_dt_quot.ML") |
8 ("nominal_dt_supp.ML") |
|
9 begin |
8 begin |
10 |
9 |
11 use "nominal_dt_rawperm.ML" |
10 use "nominal_dt_rawperm.ML" |
12 ML {* open Nominal_Dt_RawPerm *} |
11 ML {* open Nominal_Dt_RawPerm *} |
13 |
12 |
18 ML {* open Nominal_Dt_Alpha *} |
17 ML {* open Nominal_Dt_Alpha *} |
19 |
18 |
20 use "nominal_dt_quot.ML" |
19 use "nominal_dt_quot.ML" |
21 ML {* open Nominal_Dt_Quot *} |
20 ML {* open Nominal_Dt_Quot *} |
22 |
21 |
23 use "nominal_dt_supp.ML" |
|
24 ML {* open Nominal_Dt_Supp *} |
|
25 |
22 |
26 section{* Interface for nominal_datatype *} |
23 section{* Interface for nominal_datatype *} |
27 |
24 |
28 ML {* |
25 ML {* |
29 (* attributes *) |
26 (* attributes *) |