Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/MathEngBasic/mstools.sml
changeset 60565 f92963a33fe3
parent 60559 aba19e46dd84
child 60583 da7dd260f66e
equal deleted inserted replaced
60564:90ea835c07b3 60565:f92963a33fe3 
    18 "-----------------------------------------------------------------------------------------------";
 
    18 "-----------------------------------------------------------------------------------------------";
 
    19 
    19 
    20 "----------- fun Input_Descript.join -- fun Input_Descript.split -------------------------------";
 
    20 "----------- fun Input_Descript.join -- fun Input_Descript.split -------------------------------";
 
    21 "----------- fun Input_Descript.join -- fun Input_Descript.split -------------------------------";
 
    21 "----------- fun Input_Descript.join -- fun Input_Descript.split -------------------------------";
 
    22 "----------- fun Input_Descript.join -- fun Input_Descript.split -------------------------------";
 
    22 "----------- fun Input_Descript.join -- fun Input_Descript.split -------------------------------";
 
    23 (*val t = TermC.str2term "maximum A"; 
    23 (*val t = TermC.parse_test @{context} "maximum A"; 
    24 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
 
    24 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
 
    25 val it = "maximum A" : cterm
 
    25 val it = "maximum A" : cterm
 
    26 > val t = TermC.str2term "fixedValues [r=Arbfix]"; 
    26 > val t = TermC.parse_test @{context} "fixedValues [r=Arbfix]"; 
    27 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
 
    27 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
 
    28 "fixedValues [r = Arbfix]"
 
    28 "fixedValues [r = Arbfix]"
 
    29 > val t = TermC.str2term "valuesFor [a]"; 
    29 > val t = TermC.parse_test @{context} "valuesFor [a]"; 
    30 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
 
    30 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
 
    31 "valuesFor [a]"
 
    31 "valuesFor [a]"
 
    32 > val t = TermC.str2term "valuesFor [a,b]"; 
    32 > val t = TermC.parse_test @{context} "valuesFor [a,b]"; 
    33 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
 
    33 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
 
    34 "valuesFor [a, b]"
 
    34 "valuesFor [a, b]"
 
    35 > val t = TermC.str2term "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"; 
    35 > val t = TermC.parse_test @{context} "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"; 
    36 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
 
    36 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
 
    37 relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]"
 
    37 relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]"
 
    38 > val t = TermC.str2term "boundVariable a";
 
    38 > val t = TermC.parse_test @{context} "boundVariable a";
 
    39 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
 
    39 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
 
    40 "boundVariable a"
 
    40 "boundVariable a"
 
    41 > val t = TermC.str2term "interval {x::real. 0 <= x & x <= 2*r}"; 
    41 > val t = TermC.parse_test @{context} "interval {x::real. 0 <= x & x <= 2*r}"; 
    42 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
 
    42 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
 
    43 "interval {x. 0 <= x & x <= 2 * r}"
 
    43 "interval {x. 0 <= x & x <= 2 * r}"
 
    44 
    44 
    45 > val t = TermC.str2term "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))"; 
    45 > val t = TermC.parse_test @{context} "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))"; 
    46 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
 
    46 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
 
    47 "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"
 
    47 "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"
 
    48 > val t = TermC.str2term "solveFor x"; 
    48 > val t = TermC.parse_test @{context} "solveFor x"; 
    49 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
 
    49 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
 
    50 "solveFor x"
 
    50 "solveFor x"
 
    51 > val t = TermC.str2term "errorBound (eps=0)"; 
    51 > val t = TermC.parse_test @{context} "errorBound (eps=0)"; 
    52 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
 
    52 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
 
    53 "errorBound (eps = 0)"
 
    53 "errorBound (eps = 0)"
 
    54 > val t = TermC.str2term "solutions L";
 
    54 > val t = TermC.parse_test @{context} "solutions L";
 
    55 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
 
    55 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
 
    56 "solutions L"
 
    56 "solutions L"
 
    57 
    57 
    58 before 6.5.03:
 
    58 before 6.5.03:
 
    59 > val t = (Thm.term_of o the o (TermC.parse thy)) "testdscforlist [#1]";
 
    59 > val t = (Thm.term_of o the o (TermC.parse thy)) "testdscforlist [#1]";
 
   103 val it = false : bool*)
 
   103 val it = false : bool*)
 
   104 "----------- fun pbl_ids -----------------------------------------------------------------------";
 
   104 "----------- fun pbl_ids -----------------------------------------------------------------------";
 
   105 "----------- fun pbl_ids -----------------------------------------------------------------------";
 
   105 "----------- fun pbl_ids -----------------------------------------------------------------------";
 
   106 "----------- fun pbl_ids -----------------------------------------------------------------------";
 
   106 "----------- fun pbl_ids -----------------------------------------------------------------------";
 
   107 (*
 
   107 (*
 
   108 val t as t1 $ t2 = TermC.str2term "antiDerivativeName M_b";
 
   108 val t as t1 $ t2 = TermC.parse_test @{context} "antiDerivativeName M_b";
 
   109 pbl_ids ctxt t1 t2;
 
   109 pbl_ids ctxt t1 t2;
 
   110 
   110 
   111   val t = (Thm.term_of o the o (TermC.parse thy)) "fixedValues [r=Arbfix]";
 
   111   val t = (Thm.term_of o the o (TermC.parse thy)) "fixedValues [r=Arbfix]";
 
   112   val (d,argl) = strip_comb t;
 
   112   val (d,argl) = strip_comb t;
 
   113   Input_Descript.is_a d;                      (*see Input_Descript.split*)
 
   113   Input_Descript.is_a d;                      (*see Input_Descript.split*)
wneuper/isa