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 Walther Neuper <neuper@ist.tugraz.at>
Wed, 23 Mar 2011 17:20:39 +0100
branchdecompose-isar
changeset 41943 f33f6959948b
parent 38050 4c52ad406c20
child 42206 83165a8623dc
permissions -rw-r--r--
make Test_Isac.thy run in jEdit; intermed.

jEdit behaves differently from emacs in file dependencies.
Test_Isac.thy runs in emacs now.
For jEdit different uses seem appropriate; done in next step. 
     1 (* testexamples for LogExp, logarithms and exponential functions and terms

     2 

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

     4 *)

     5 

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

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

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

     9 "----------- setup presentation innsbruck ------------------------";

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

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

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

    13 

    14 (*=== inhibit exn ?=============================================================

    15 val thy = LogExp.thy;

    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 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

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

    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 case nxt of ("Apply_Method",_) => ()

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

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

    54 

    55 

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

    61 

    62 *-------------------------------------------------------------------*)

    63 ===== inhibit exn ?===========================================================*)
wneuper/isa