Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Knowledge/logexp.sml
author Thomas Leh <t.leh@gmx.at>
Tue, 26 Jul 2011 16:50:27 +0200
branchdecompose-isar
changeset 42206 83165a8623dc
parent 41943 f33f6959948b
child 42321 e68b4b4f0fac
permissions -rw-r--r--
tuned 
     1 

     2 (* testexamples for LogExp, logarithms and exponential functions and terms

     3 

     4 use"../smltest/IsacKnowledge/logexp.sml";

     5 *)

     6 

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

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

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

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

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

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

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

    14 

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

    16 

    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 !

    24 

    25 equality_power;

    26 exp_invers_log;

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

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

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

    30 *)

    31 

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

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

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

    35 atomty t;

    36 

    37 

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

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

    40   ("Isac",["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;

    55 

    56 

    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 show_pt pt;

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

    63
wneuper/isa