wneuper/isa: test/Tools/isac/Knowledge/equation.sml@c0a775618258

     1 (* tests on the equation solver

     2    author: Walther Neuper 070703

     3    (c) due to copyright terms

     4 *)

     6 "-----------------------------------------------------------------";

     7 "table of contents -----------------------------------------------";

     8 "-----------------------------------------------------------------";

     9 "----------- CAS input -------------------------------------------";

    10 "-----------------------------------------------------------------";

    11 "-----------------------------------------------------------------";

    12 "-----------------------------------------------------------------";

    14 val thy = @{theory "Equation"}

    15 val ctxt = Proof_Context.init_global thy;

    17 "----------- CAS input -------------------------------------------";

    18 "----------- CAS input -------------------------------------------";

    19 "----------- CAS input -------------------------------------------";

    20 States.reset ();

    21 CalcTree [([], References.empty)];

    22 Iterator 1;

    23 moveActiveRoot 1;

    24 replaceFormula 1 "solve (x+1=2, x)";

    25 (*========== inhibit exn 130719 Isabelle2013 ===================================loops

    26 autoCalculate 1 CompleteCalc;

    27 val ((pt,p),_) = States.get_calc 1;

    28 val Form res = (#1 o ME_Misc.pt_extract) (pt, ([],Res));

    29 Test_Tool.show_pt pt;

    30 if p = ([], Res) andalso UnparseC.term res = "[x = 1]" then ()

    31 else error "equation.sml behav.changed for CAS solve (x+1=2, x))";

    32 ============ inhibit exn 130719 Isabelle2013 =================================*)

author	wneuper <Walther.Neuper@jku.at>
	Sun, 11 Sep 2022 14:31:15 +0200
changeset 60549	c0a775618258
parent 60428	203438ff792f
child 60571	19a172de0bb5
permissions	-rw-r--r--