test/Tools/isac/OLDTESTS/scriptnew.sml
changeset 59585 0bb418c3855a
parent 59497 8952c43fdce3
child 59627 2679ff6624eb
     1.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml	Thu Aug 22 15:56:48 2019 +0200
     1.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml	Thu Aug 22 16:48:04 2019 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4     {rew_ord'="tless_true",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
     1.5      crls=tval_rls, errpats = [], nrls=e_rls(*,
     1.6      asm_rls=[],asm_thm=[]*)},
     1.7 - "Script Testterm (g_::real) =   \
     1.8 + "Program Testterm (g_::real) =   \
     1.9   \Repeat\
    1.10   \  ((Repeat (Rewrite rmult_1 False)) Or\
    1.11   \   (Repeat (Rewrite rmult_0 False)) Or\
    1.12 @@ -109,7 +109,7 @@
    1.13  		    [Calc ("Test.contains'_root", eval_contains_root"")],
    1.14      prls=e_rls,calc=[], crls=tval_rls, errpats = [], nrls=e_rls
    1.15  		  (*,asm_rls=[],asm_thm=[("square_equation_left","")]*)},
    1.16 - "Script Testeq (e_e::bool) =                                        \
    1.17 + "Program Testeq (e_e::bool) =                                        \
    1.18     \(While (contains_root e_e) Do                                     \
    1.19     \((Try (Repeat (Rewrite rroot_square_inv False))) @@    \
    1.20     \  (Try (Repeat (Rewrite square_equation_left True))) @@ \
    1.21 @@ -167,7 +167,7 @@
    1.22  		    [Calc ("Test.contains'_root",eval_contains_root"")],
    1.23      prls=e_rls,calc=[], crls=tval_rls, errpats = [], nrls=e_rls
    1.24  		  (*,asm_rls=[],asm_thm=[("square_equation_left","")]*)},
    1.25 -   "Script Testeq2 (e_e::bool) =                                        \
    1.26 +   "Program Testeq2 (e_e::bool) =                                        \
    1.27     \(let e_e =\
    1.28     \  ((While (contains_root e_e) Do                                     \
    1.29     \   (Rewrite square_equation_left True))\
    1.30 @@ -484,7 +484,7 @@
    1.31  
    1.32  (*GoOn.5.03. script with Map, Subst (biquadr.equ.)
    1.33  val scr = Prog ((inst_abs o Thm.term_of o the o (parse thy))
    1.34 -    "Script Biquadrat_poly (e_e::bool) (v_::real) =                       \
    1.35 +    "Program Biquadrat_poly (e_e::bool) (v_::real) =                       \
    1.36      \(let e_e = Substitute [(v_^^^4, v_0_^^^2),(v_^^^2, v_0_)] e_;        \ 
    1.37      \     L_0_ = (SubProblem (PolyEqX,[univariate,equation], [no_met])   \
    1.38      \             [BOOL e_e, REAL v_0_]);                               \