equal
deleted
inserted
replaced
56 use "print_exn_G.sml" |
56 use "print_exn_G.sml" |
57 ML {* writeln "**** build math-engine complete **************************" *} |
57 ML {* writeln "**** build math-engine complete **************************" *} |
58 |
58 |
59 ML {* writeln "**** build the Knowledge *********************************" *} |
59 ML {* writeln "**** build the Knowledge *********************************" *} |
60 (*use_thy "Knowledge/Typefix"*) |
60 (*use_thy "Knowledge/Typefix"*) |
61 use_thy "Knowledge/Delete" |
61 (*use_thy "Knowledge/Delete" |
62 use_thy "Knowledge/Descript" |
62 use_thy "Knowledge/Descript" |
63 use_thy "Knowledge/Atools" |
63 use_thy "Knowledge/Atools" |
64 use_thy "Knowledge/Simplify" |
64 use_thy "Knowledge/Simplify" |
65 use_thy "Knowledge/Poly" |
65 use_thy "Knowledge/Poly" |
66 |
66 *) |
67 ML {* |
|
68 val r = @{thm divide_minus1}; |
|
69 *} |
|
70 lemma "(x::real) / -1 = - x" |
|
71 by (rule divide_minus1) |
|
72 |
|
73 |
|
74 use_thy "Knowledge/Rational" |
67 use_thy "Knowledge/Rational" |
75 |
68 |
76 ML {* |
69 ML {* |
77 val ------+ = "123"; |
70 111; |
78 *} |
71 *} |
|
72 |
79 |
73 |
80 text {*------------------------------------------*} |
74 text {*------------------------------------------*} |
81 (* |
75 (* |
82 use_thy "Knowledge/PolyMinus" |
76 use_thy "Knowledge/PolyMinus" |
83 use_thy "Knowledge/Equation" |
77 use_thy "Knowledge/Equation" |