1.1 --- a/src/Tools/isac/IsacKnowledge/DiffApp.sml	Wed Aug 25 15:15:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,105 +0,0 @@
     1.4 -(* = DiffAppl.ML
     1.5 -   +++ outcommented tests
     1.6 -*)
     1.7 -
     1.8 -
     1.9 -theory' := overwritel (!theory', [("DiffAppl.thy",DiffAppl.thy)]);
    1.10 -
    1.11 -(* 
    1.12 -> get_pbt ["DiffAppl.thy","maximum_of","function"];
    1.13 -> get_met ("Script.thy","max_on_interval_by_calculus");
    1.14 -> !pbltypes;
    1.15 -  *)
    1.16 -pbltypes:= overwritel (!pbltypes,
    1.17 -[
    1.18 - prep_pbt DiffAppl.thy
    1.19 - (["DiffAppl.thy","maximum_of","function"],
    1.20 -  [("#Given" ,"fixedValues fix_"),
    1.21 -   ("#Find"  ,"maximum m_"),
    1.22 -   ("#Find"  ,"valuesFor vs_"),
    1.23 -   ("#Relate","relations rs_")  (*,
    1.24 -   ("#where" ,"foldl (op&) True (map (Not o ((op<=) #0) o Rhs) fix_)"),
    1.25 -   ("#with"  ,"Ex_frees ((foldl (op &) True rs_) &  \
    1.26 -    \ (ALL m'. (subst (m_,m') (foldl (op &) True rs_) \
    1.27 -    \            --> m' <= m_)))")    *)
    1.28 -  ]),
    1.29 -
    1.30 - prep_pbt DiffAppl.thy
    1.31 - (["DiffAppl.thy","make","function"]:pblID,
    1.32 -  [("#Given" ,"functionOf f_"),
    1.33 -   ("#Given" ,"boundVariable v_"),
    1.34 -   ("#Given" ,"equalities eqs_"),
    1.35 -   ("#Find"  ,"functionTerm f_0_")
    1.36 -  ]),
    1.37 -
    1.38 - prep_pbt DiffAppl.thy
    1.39 - (["DiffAppl.thy","on_interval","maximum_of","function"]:pblID,
    1.40 -  [("#Given" ,"functionTerm t_"),
    1.41 -   ("#Given" ,"boundVariable v_"),
    1.42 -   ("#Given" ,"interval itv_"),
    1.43 -   ("#Find"  ,"maxArgument v_0_")
    1.44 -  ]),
    1.45 -
    1.46 - prep_pbt DiffAppl.thy
    1.47 - (["DiffAppl.thy","find_values","tool"]:pblID,
    1.48 -  [("#Given" ,"maxArgument ma_"),
    1.49 -   ("#Given" ,"functionTerm f_"),
    1.50 -   ("#Given" ,"boundVariable v_"),
    1.51 -   ("#Find"  ,"valuesFor vls_"),
    1.52 -   ("#Relate","additionalRels rs_")
    1.53 -  ])
    1.54 -]);
    1.55 -
    1.56 -
    1.57 -methods:= overwritel (!methods,
    1.58 -[
    1.59 - (("DiffAppl.thy","max_by_calculus"):metID,
    1.60 -  {ppc = prep_met DiffAppl.thy
    1.61 -   [("#Given" ,"fixedValues fix_"),
    1.62 -    ("#Given" ,"boundVariable v_"),
    1.63 -    ("#Given" ,"interval itv_"),
    1.64 -    ("#Given" ,"errorBound err_"),
    1.65 -    ("#Find"  ,"maximum m_"),
    1.66 -    ("#Find"  ,"valuesFor vs_"),
    1.67 -    ("#Relate","relations rs_")
    1.68 -    ],
    1.69 -   rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
    1.70 -   scr=EmptyScr} : met),
    1.71 -
    1.72 - (("DiffAppl.thy","make_fun_by_new_variable"):metID,
    1.73 -  {ppc = prep_met DiffAppl.thy
    1.74 -   [("#Given" ,"functionOf f_"),
    1.75 -    ("#Given" ,"boundVariable v_"),
    1.76 -    ("#Given" ,"equalities eqs_"),
    1.77 -    ("#Find"  ,"functionTerm f_0_")
    1.78 -    ],
    1.79 -   rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
    1.80 -   scr=EmptyScr} : met),
    1.81 -
    1.82 - (("DiffAppl.thy","make_fun_by_explicit"):metID,
    1.83 -  {ppc = prep_met DiffAppl.thy
    1.84 -   [("#Given" ,"functionOf f_"),
    1.85 -    ("#Given" ,"boundVariable v_"),
    1.86 -    ("#Given" ,"equalities eqs_"),
    1.87 -    ("#Find"  ,"functionTerm f_0_")
    1.88 -    ],
    1.89 -   rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
    1.90 -   scr=EmptyScr} : met),
    1.91 -  
    1.92 - (("DiffAppl.thy","max_on_interval_by_calculus"):metID,
    1.93 -  {ppc = prep_met DiffAppl.thy
    1.94 -   [("#Given" ,"functionTerm t_"),
    1.95 -    ("#Given" ,"boundVariable v_"),
    1.96 -    ("#Given" ,"interval itv_"),
    1.97 -    ("#Given" ,"errorBound err_"),
    1.98 -    ("#Find"  ,"maxArgument v_0_")
    1.99 -    ],
   1.100 -   rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
   1.101 -   scr=EmptyScr} : met),
   1.102 -
   1.103 - (("DiffAppl.thy","find_values"):metID,
   1.104 -  {ppc = prep_met DiffAppl.thy
   1.105 -   [],
   1.106 -   rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
   1.107 -   scr=EmptyScr} : met)
   1.108 -]);