src/Tools/isac/Knowledge/Diff.thy
branchisac-update-Isa09-2
changeset 37982 66f3570ba808
parent 37981 b2877b9d455a
child 37983 03bfbc480107
     1.1 --- a/src/Tools/isac/Knowledge/Diff.thy	Mon Sep 06 15:09:37 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Diff.thy	Mon Sep 06 15:53:18 2010 +0200
     1.3 @@ -281,7 +281,7 @@
     1.4      ],
     1.5     {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls, 
     1.6      prls=e_rls, crls = Atools_erls, nrls = norm_diff},
     1.7 -"Script DiffScr (f_::real) (v_::real) =                          " ^
     1.8 +"Script DiffScr (f_::real) (v_v::real) =                          " ^
     1.9  " (let f'_ = Take (d_d v_v f_)                                    " ^
    1.10  " in (((Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@    " ^
    1.11  " (Repeat                                                        " ^
    1.12 @@ -313,7 +313,7 @@
    1.13      ],
    1.14     {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls,
    1.15      prls=e_rls, crls = Atools_erls, nrls = norm_diff},
    1.16 -"Script DiffScr (f_::real) (v_::real) =                          " ^
    1.17 +"Script DiffScr (f_::real) (v_v::real) =                          " ^
    1.18  " (let f'_ = Take (d_d v_v f_)                                    " ^
    1.19  " in ((     " ^
    1.20  " (Repeat                                                        " ^
    1.21 @@ -345,7 +345,7 @@
    1.22    ],
    1.23     {rew_ord'="tless_true", rls' = erls_diff, calc = [], 
    1.24      srls = srls_diff, prls=e_rls, crls=Atools_erls, nrls = norm_diff},
    1.25 -"Script DiffEqScr (f_::bool) (v_::real) =                          " ^
    1.26 +"Script DiffEqScr (f_::bool) (v_v::real) =                          " ^
    1.27  " (let f'_ = Take ((primed (lhs f_)) = d_d v_v (rhs f_))            " ^
    1.28  " in (((Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@      " ^
    1.29  " (Repeat                                                          " ^
    1.30 @@ -378,7 +378,7 @@
    1.31      ],
    1.32     {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, prls=e_rls,
    1.33      crls=Atools_erls, nrls = norm_Rational},
    1.34 -"Script DiffScr (f_::real) (v_::real) =                          " ^
    1.35 +"Script DiffScr (f_::real) (v_v::real) =                          " ^
    1.36  " (let f'_ = Take (d_d v_v f_)                                    " ^
    1.37  " in ((Try (Rewrite_Set norm_Rational False)) @@                 " ^
    1.38  "     (Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@     " ^