equal
deleted
inserted
replaced
25 |
25 |
26 use_thy "Ord"; |
26 use_thy "Ord"; |
27 use_thy "subset"; |
27 use_thy "subset"; |
28 use "hologic.ML"; |
28 use "hologic.ML"; |
29 use "typedef.ML"; |
29 use "typedef.ML"; |
30 use_thy "Prod"; |
|
31 use_thy "Sum"; |
30 use_thy "Sum"; |
32 use_thy "Gfp"; |
31 use_thy "Gfp"; |
33 use_thy "Nat"; |
32 use_thy "RelPow"; |
34 |
33 |
35 use "datatype.ML"; |
34 use "datatype.ML"; |
36 use "ind_syntax.ML"; |
35 use "ind_syntax.ML"; |
37 use "add_ind_def.ML"; |
36 use "add_ind_def.ML"; |
38 use "intr_elim.ML"; |
37 use "intr_elim.ML"; |