equal
deleted
inserted
replaced
50 use "Tools/datatype_rep_proofs.ML"; |
50 use "Tools/datatype_rep_proofs.ML"; |
51 use "Tools/datatype_abs_proofs.ML"; |
51 use "Tools/datatype_abs_proofs.ML"; |
52 use "Tools/datatype_package.ML"; |
52 use "Tools/datatype_package.ML"; |
53 use "Tools/primrec_package.ML"; |
53 use "Tools/primrec_package.ML"; |
54 use_thy "Datatype"; |
54 use_thy "Datatype"; |
|
55 use_thy "Numeral"; |
55 |
56 |
56 use "Tools/record_package.ML"; |
57 use "Tools/record_package.ML"; |
57 use_thy "Record"; |
58 use_thy "Record"; |
58 |
59 |
59 (*TFL: recursive function definitions*) |
60 (*TFL: recursive function definitions*) |