equal
deleted
inserted
replaced
59 |
59 |
60 ML {* writeln "**** build the Knowledge *********************************" *} |
60 ML {* writeln "**** build the Knowledge *********************************" *} |
61 use_thy "Knowledge/Typefix" |
61 use_thy "Knowledge/Typefix" |
62 use_thy "Knowledge/Descript" |
62 use_thy "Knowledge/Descript" |
63 |
63 |
64 ML {* |
|
65 |
|
66 111; |
|
67 *} |
|
68 |
|
69 use_thy "Knowledge/Atools" |
64 use_thy "Knowledge/Atools" |
70 |
65 |
71 |
66 |
72 ML {* |
67 ML {* |
73 val str = "1234567890"; |
68 111; |
74 *} |
69 *} |
75 |
70 |
76 (* |
71 (* |
77 use_thy "Knowledge/Simplify" |
72 use_thy "Knowledge/Simplify" |
78 use_thy "Knowledge/Poly" |
73 use_thy "Knowledge/Poly" |