101 |
101 |
102 *) |
102 *) |
103 "----------------------------------------------------------"; |
103 "----------------------------------------------------------"; |
104 val fod = make_deriv Isac.thy Atools_erls |
104 val fod = make_deriv Isac.thy Atools_erls |
105 ((#rules o rep_rls) Test_simplify) |
105 ((#rules o rep_rls) Test_simplify) |
106 (sqrt_right false ProtoPure.thy) NONE |
106 (sqrt_right false (theory "Pure")) NONE |
107 (str2term "x + 1 + -1 * 2 = 0"); |
107 (str2term "x + 1 + -1 * 2 = 0"); |
108 (writeln o trtas2str) fod; |
108 (writeln o trtas2str) fod; |
109 |
109 |
110 val ifod = make_deriv Isac.thy Atools_erls |
110 val ifod = make_deriv Isac.thy Atools_erls |
111 ((#rules o rep_rls) Test_simplify) |
111 ((#rules o rep_rls) Test_simplify) |
112 (sqrt_right false ProtoPure.thy) NONE |
112 (sqrt_right false (theory "Pure")) NONE |
113 (str2term "-2 * 1 + (1 + x) = 0"); |
113 (str2term "-2 * 1 + (1 + x) = 0"); |
114 (writeln o trtas2str) ifod; |
114 (writeln o trtas2str) ifod; |
115 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2; |
115 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2; |
116 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod); |
116 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod); |
117 val der = fod' @ (map rev_deriv' rifod'); |
117 val der = fod' @ (map rev_deriv' rifod'); |