remove comments from (*ML_file ?..?*) in Test_Isac_Short.thy
authorwneuper <walther.neuper@jku.at>
Wed, 04 Aug 2021 17:34:47 +0200
changeset 603503e9b709fc755
parent 60349 79900b7d3fd3
child 60351 d74e7e33db35
remove comments from (*ML_file ?..?*) in Test_Isac_Short.thy

?
test/Tools/isac/Knowledge/diff.sml
test/Tools/isac/Knowledge/integrate.sml
test/Tools/isac/Test_Isac_Short.thy
     1.1 --- a/test/Tools/isac/Knowledge/diff.sml	Wed Aug 04 10:15:55 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/diff.sml	Wed Aug 04 17:34:47 2021 +0200
     1.3 @@ -280,20 +280,25 @@
     1.4  
     1.5  val rls = diff_sym_conv;
     1.6  
     1.7 +(*/--------------- TOODOO.1 ? --------------------------------------------\* )
     1.8  val t = TermC.str2term "2 * x \<up> - 2";
     1.9  val SOME (t, _) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t;
    1.10  if UnparseC.term t = "2 / x \<up> 2" then () else error "diff.sml sym 1/x";
    1.11 +( *\--------------- TOODOO.1 ? --------------------------------------------/*)
    1.12  
    1.13  
    1.14  val t = TermC.str2term "x \<up> (3 / 2)";
    1.15  val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t;
    1.16  if UnparseC.term t = "sqrt (x \<up> 3)" then ((*..wrong rewrite*)) else error"diff.sml sym x \<up> 1/x";
    1.17  
    1.18 +(*/--------------- TOODOO.1 ? --------------------------------------------\* )
    1.19  val t = TermC.str2term "2 * x \<up> (-3 / 2)";
    1.20  val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term t;
    1.21  if UnparseC.term t ="2 / sqrt (x \<up> 3)"then()else error"diff.sml sym x \<up> - 1/x";
    1.22 +( *\--------------- TOODOO.1 ? --------------------------------------------/*)
    1.23  
    1.24  
    1.25 +(*/--------------- TOODOO.1 ? --------------------------------------------\* )
    1.26  "----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";
    1.27  "----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";
    1.28  "----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";
    1.29 @@ -311,6 +316,7 @@
    1.30  if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = 
    1.31  			  "1 + 2 * x + - 1 / x \<up> 2 + - 4 / x \<up> 3" then ()
    1.32  else error "diff.sml: differentiate_on_R 2/x \<up> 2 changed";
    1.33 +( *\--------------- TOODOO.1 ? --------------------------------------------/*)
    1.34  
    1.35  "---------------------------------------------------------";
    1.36  reset_states ();
    1.37 @@ -367,6 +373,7 @@
    1.38  if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "15 * x \<up> 14"
    1.39  then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
    1.40  
    1.41 +(*/--------------- TOODOO.1 ? loops with repair ord_make_polynomial_in-----------\* )
    1.42  "----------- autoCalculate differentiate_equality -------";
    1.43  "----------- autoCalculate differentiate_equality -------";
    1.44  "----------- autoCalculate differentiate_equality -------";
    1.45 @@ -379,6 +386,7 @@
    1.46  moveActiveRoot 1;
    1.47  autoCalculate 1 CompleteCalc;
    1.48  val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
    1.49 +( *\--------------- TOODOO.1 ? --------------------------------------------/*)
    1.50  
    1.51  "----------- tests for examples -------------------------";
    1.52  "----------- tests for examples -------------------------";
     2.1 --- a/test/Tools/isac/Knowledge/integrate.sml	Wed Aug 04 10:15:55 2021 +0200
     2.2 +++ b/test/Tools/isac/Knowledge/integrate.sml	Wed Aug 04 17:34:47 2021 +0200
     2.3 @@ -473,7 +473,7 @@
     2.4  val (p,_,f,nxt,_,pt) = me nxt p c pt;
     2.5  val (p,_,f,nxt,_,pt) = me nxt p c pt;
     2.6  val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
     2.7 -if f2str f = "Q x = c + - q_0 * x" then() 
     2.8 +if f2str f = "Q x = c + - 1 * q_0 * x" then() 
     2.9  else error "integrate.sml: method [diff,integration,named] .Q";
    2.10  
    2.11  
     3.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Wed Aug 04 10:15:55 2021 +0200
     3.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Wed Aug 04 17:34:47 2021 +0200
     3.3 @@ -294,23 +294,23 @@
     3.4    ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
     3.5  (*ML_file "Knowledge/partial_fractions.sml"  hangs with ML_system_64 = "true"---Test_Isac_Short*)
     3.6  (*ML_file "Knowledge/polyeq-1.sml"                          TOODOO.1 error inherited from root.sml*)
     3.7 -(*ML_file "Knowledge/polyeq-2.sml"                                              Test_Isac_Short*)
     3.8 +(*ML_file "Knowledge/polyeq-2.sml"                          TOODOO.1            Test_Isac_Short*)
     3.9  (*ML_file "Knowledge/rlang.sml"     much to clean up, similar tests in other files     *)
    3.10    ML_file "Knowledge/calculus.sml"
    3.11    ML_file "Knowledge/trig.sml"
    3.12  (*ML_file "Knowledge/logexp.sml"    not included as stuff for presentation of authoring*) 
    3.13 -(*ML_file "Knowledge/diff.sml" TOODOO loops with repair ord_make_polynomial_in*)
    3.14 -(*ML_file "Knowledge/integrate.sml" TOODOO broken with repair ord_make_polynomial_in*)
    3.15 +  ML_file "Knowledge/diff.sml"
    3.16 +  ML_file "Knowledge/integrate.sml"
    3.17    ML_file "Knowledge/eqsystem-1.sml"
    3.18    ML_file "Knowledge/eqsystem-2.sml"
    3.19    ML_file "Knowledge/test.sml"
    3.20    ML_file "Knowledge/polyminus.sml"
    3.21    ML_file "Knowledge/vect.sml"
    3.22    ML_file "Knowledge/diffapp.sml"        (* postponed to dev. specification | TP-prog. *)
    3.23 -(*ML_file "Knowledge/biegelinie-1.sml"                   (**) requires integrate.sml, eqsystem.sml*)
    3.24 +(*ML_file "Knowledge/biegelinie-1.sml"          (**) TOODOO.1 requires integrate.sml, eqsystem.sml*)
    3.25  (*ML_file "Knowledge/biegelinie-2.sml"                                          Test_Isac_Short*)
    3.26  (*ML_file "Knowledge/biegelinie-3.sml"                                          Test_Isac_Short*)
    3.27 -(*ML_file "Knowledge/biegelinie-4.sml"                   (**) requires integrate.sml, eqsystem.sml*)
    3.28 +(*ML_file "Knowledge/biegelinie-4.sml"          (**) TOODOO.1 requires integrate.sml, eqsystem.sml*)
    3.29    ML_file "Knowledge/algein.sml"
    3.30    ML_file "Knowledge/diophanteq.sml"
    3.31  (*ML_file "Knowledge/inverse_z_transform.sml"hangs with ML_system_64 = "true"---Test_Isac_Short*)