|
neuper@37906
|
1 |
(* tests on the equation solver
|
|
neuper@41943
|
2 |
author: Walther Neuper 070703
|
|
neuper@37906
|
3 |
(c) due to copyright terms
|
|
neuper@37906
|
4 |
*)
|
|
neuper@37906
|
5 |
|
|
neuper@37906
|
6 |
"-----------------------------------------------------------------";
|
|
neuper@37906
|
7 |
"table of contents -----------------------------------------------";
|
|
neuper@37906
|
8 |
"-----------------------------------------------------------------";
|
|
neuper@37906
|
9 |
"----------- CAS input -------------------------------------------";
|
|
neuper@37906
|
10 |
"-----------------------------------------------------------------";
|
|
neuper@37906
|
11 |
"-----------------------------------------------------------------";
|
|
neuper@37906
|
12 |
"-----------------------------------------------------------------";
|
|
neuper@37906
|
13 |
|
|
neuper@42395
|
14 |
val thy = @{theory "Equation"}
|
|
neuper@48761
|
15 |
val ctxt = Proof_Context.init_global thy;
|
|
neuper@37906
|
16 |
|
|
neuper@37906
|
17 |
"----------- CAS input -------------------------------------------";
|
|
neuper@37906
|
18 |
"----------- CAS input -------------------------------------------";
|
|
neuper@37906
|
19 |
"----------- CAS input -------------------------------------------";
|
|
s1210629013@55445
|
20 |
reset_states ();
|
|
walther@59903
|
21 |
CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
|
|
neuper@37906
|
22 |
Iterator 1;
|
|
neuper@37906
|
23 |
moveActiveRoot 1;
|
|
neuper@37906
|
24 |
replaceFormula 1 "solve (x+1=2, x)";
|
|
neuper@52065
|
25 |
(*========== inhibit exn 130719 Isabelle2013 ===================================loops
|
|
wneuper@59248
|
26 |
autoCalculate 1 CompleteCalc;
|
|
neuper@37906
|
27 |
val ((pt,p),_) = get_calc 1;
|
|
neuper@37906
|
28 |
val Form res = (#1 o pt_extract) (pt, ([],Res));
|
|
neuper@37906
|
29 |
show_pt pt;
|
|
walther@59868
|
30 |
if p = ([], Res) andalso UnparseC.term res = "[x = 1]" then ()
|
|
neuper@38031
|
31 |
else error "equation.sml behav.changed for CAS solve (x+1=2, x))";
|
|
neuper@52065
|
32 |
============ inhibit exn 130719 Isabelle2013 =================================*)
|
|
neuper@42395
|
33 |
|