1.1 --- a/src/Tools/isac/Knowledge/DiffApp.sml	Wed Sep 08 17:20:03 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/DiffApp.sml	Wed Sep 08 17:49:36 2010 +0200
     1.3 @@ -14,13 +14,13 @@
     1.4  [
     1.5   prep_pbt DiffAppl.thy
     1.6   (["DiffAppl","maximum_of","function"],
     1.7 -  [("#Given" ,"fixedValues fix_"),
     1.8 +  [("#Given" ,"fixedValues f_ix"),
     1.9     ("#Find"  ,"maximum m_"),
    1.10 -   ("#Find"  ,"valuesFor vs_"),
    1.11 -   ("#Relate","relations rs_")  (*,
    1.12 -   ("#where" ,"foldl (op&) True (map (Not o ((op<=) #0) o Rhs) fix_)"),
    1.13 -   ("#with"  ,"Ex_frees ((foldl (op &) True rs_) &  \
    1.14 -    \ (ALL m'. (subst (m_,m') (foldl (op &) True rs_) \
    1.15 +   ("#Find"  ,"valuesFor v_s"),
    1.16 +   ("#Relate","relations r_s")  (*,
    1.17 +   ("#where" ,"foldl (op&) True (map (Not o ((op<=) #0) o Rhs) f_ix)"),
    1.18 +   ("#with"  ,"Ex_frees ((foldl (op &) True r_s) &  \
    1.19 +    \ (ALL m'. (subst (m_,m') (foldl (op &) True r_s) \
    1.20      \            --> m' <= m_)))")    *)
    1.21    ]),
    1.22  
    1.23 @@ -37,7 +37,7 @@
    1.24    [("#Given" ,"functionTerm t_"),
    1.25     ("#Given" ,"boundVariable v_v"),
    1.26     ("#Given" ,"interval itv_"),
    1.27 -   ("#Find"  ,"maxArgument v_0_")
    1.28 +   ("#Find"  ,"maxArgument v_0")
    1.29    ]),
    1.30  
    1.31   prep_pbt DiffAppl.thy
    1.32 @@ -46,7 +46,7 @@
    1.33     ("#Given" ,"functionTerm f_f"),
    1.34     ("#Given" ,"boundVariable v_v"),
    1.35     ("#Find"  ,"valuesFor vls_"),
    1.36 -   ("#Relate","additionalRels rs_")
    1.37 +   ("#Relate","additionalRels r_s")
    1.38    ])
    1.39  ]);
    1.40  
    1.41 @@ -55,13 +55,13 @@
    1.42  [
    1.43   (("DiffAppl","max_by_calculus"):metID,
    1.44    {ppc = prep_met DiffAppl.thy
    1.45 -   [("#Given" ,"fixedValues fix_"),
    1.46 +   [("#Given" ,"fixedValues f_ix"),
    1.47      ("#Given" ,"boundVariable v_v"),
    1.48      ("#Given" ,"interval itv_"),
    1.49      ("#Given" ,"errorBound err_"),
    1.50      ("#Find"  ,"maximum m_"),
    1.51 -    ("#Find"  ,"valuesFor vs_"),
    1.52 -    ("#Relate","relations rs_")
    1.53 +    ("#Find"  ,"valuesFor v_s"),
    1.54 +    ("#Relate","relations r_s")
    1.55      ],
    1.56     rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
    1.57     scr=EmptyScr} : met),
    1.58 @@ -92,7 +92,7 @@
    1.59      ("#Given" ,"boundVariable v_v"),
    1.60      ("#Given" ,"interval itv_"),
    1.61      ("#Given" ,"errorBound err_"),
    1.62 -    ("#Find"  ,"maxArgument v_0_")
    1.63 +    ("#Find"  ,"maxArgument v_0")
    1.64      ],
    1.65     rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
    1.66     scr=EmptyScr} : met),