wneuper/isa: test/Tools/isac/Knowledge/logexp.sml@e534316f9e07

     2 (* Title:  test/../logexp.sml

     3    Author: Walther Neuper 110320

     4    (c) copyright due to lincense terms.

     5 *)

     7 "-----------------------------------------------------------------";

     8 "table of contents -----------------------------------------------";

     9 "-----------------------------------------------------------------";

    10 "----------- setup presentation innsbruck ------------------------";

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

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

    13 "-----------------------------------------------------------------";

    15 val thy = @{theory "LogExp"};

    17 "----------- setup presentation innsbruck ------------------------";

    18 "----------- setup presentation innsbruck ------------------------";

    19 "----------- setup presentation innsbruck ------------------------";

    20 (*

    21 NOT INCLUDED IN ROOT.ML and RTEST-root.sml, since the pbl and met

    22 defined in IsacKnowledge/Test.ML are out-commented

    23 in order to allow for demonstration of authoring !

    25 equality_power;

    26 exp_invers_log;

    27 (* WN071203 ???... wrong thy ?!? because parsing with (theory "Isac_Knowledge") works ?

    28 Refine.refine ["equality ((2 log x) = 3)", "solveFor x", "solutions L"]

    29        ["equation", "test"]; *)

    30 *)

    32 val t = TermC.str2term "(2 log x)";

    33 val t = TermC.str2term "(2 log x) = 3";

    34 val t = TermC.str2term "matches ((?a log x) = ?b) ((2 log x) = 3)";

    35 TermC.atomty t;

    38 val fmz = ["equality ((2 log x) = 3)", "solveFor x", "solutions L"];

    39 val (dI',pI',mI') =

    40   ("Isac_Knowledge",["logarithmic", "univariate", "equation", "test"],

    41    ["Test", "solve_log"]);

    42 val p = e_pos'; val c = [];

    43 (*============ inhibit exn 110726 ==============================================

    44 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

    45 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    46 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    47 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    48 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    49 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    50 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    51 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    52 case nxt of ("Apply_Method",_) => ()

    53 	  | _ => error "logexp.sml setup innsbruck";

    54 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    57 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    58 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    59 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    60 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

    61 Test_Tool.show_pt pt;

    62 ============ inhibit exn 110726 ==============================================*)

author	wenzelm
	Mon, 19 Apr 2021 20:12:53 +0200
changeset 60237	e534316f9e07
parent 60230	0ca0f9363ad3
child 60565	f92963a33fe3
permissions	-rw-r--r--