1.1 --- a/src/Tools/isac/Knowledge/DiffApp.sml	Wed Sep 08 16:45:27 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/DiffApp.sml	Wed Sep 08 16:47:22 2010 +0200
     1.3 @@ -3,17 +3,17 @@
     1.4  *)
     1.5  
     1.6  
     1.7 -theory' := overwritel (!theory', [("DiffAppl.thy",DiffAppl.thy)]);
     1.8 +theory' := overwritel (!theory', [("DiffAppl",DiffAppl.thy)]);
     1.9  
    1.10  (* 
    1.11 -> get_pbt ["DiffAppl.thy","maximum_of","function"];
    1.12 -> get_met ("Script.thy","max_on_interval_by_calculus");
    1.13 +> get_pbt ["DiffAppl","maximum_of","function"];
    1.14 +> get_met ("Script","max_on_interval_by_calculus");
    1.15  > !pbltypes;
    1.16    *)
    1.17  pbltypes:= overwritel (!pbltypes,
    1.18  [
    1.19   prep_pbt DiffAppl.thy
    1.20 - (["DiffAppl.thy","maximum_of","function"],
    1.21 + (["DiffAppl","maximum_of","function"],
    1.22    [("#Given" ,"fixedValues fix_"),
    1.23     ("#Find"  ,"maximum m_"),
    1.24     ("#Find"  ,"valuesFor vs_"),
    1.25 @@ -25,7 +25,7 @@
    1.26    ]),
    1.27  
    1.28   prep_pbt DiffAppl.thy
    1.29 - (["DiffAppl.thy","make","function"]:pblID,
    1.30 + (["DiffAppl","make","function"]:pblID,
    1.31    [("#Given" ,"functionOf f_"),
    1.32     ("#Given" ,"boundVariable v_v"),
    1.33     ("#Given" ,"equalities eqs_"),
    1.34 @@ -33,7 +33,7 @@
    1.35    ]),
    1.36  
    1.37   prep_pbt DiffAppl.thy
    1.38 - (["DiffAppl.thy","on_interval","maximum_of","function"]:pblID,
    1.39 + (["DiffAppl","on_interval","maximum_of","function"]:pblID,
    1.40    [("#Given" ,"functionTerm t_"),
    1.41     ("#Given" ,"boundVariable v_v"),
    1.42     ("#Given" ,"interval itv_"),
    1.43 @@ -41,7 +41,7 @@
    1.44    ]),
    1.45  
    1.46   prep_pbt DiffAppl.thy
    1.47 - (["DiffAppl.thy","find_values","tool"]:pblID,
    1.48 + (["DiffAppl","find_values","tool"]:pblID,
    1.49    [("#Given" ,"maxArgument ma_"),
    1.50     ("#Given" ,"functionTerm f_"),
    1.51     ("#Given" ,"boundVariable v_v"),
    1.52 @@ -53,7 +53,7 @@
    1.53  
    1.54  methods:= overwritel (!methods,
    1.55  [
    1.56 - (("DiffAppl.thy","max_by_calculus"):metID,
    1.57 + (("DiffAppl","max_by_calculus"):metID,
    1.58    {ppc = prep_met DiffAppl.thy
    1.59     [("#Given" ,"fixedValues fix_"),
    1.60      ("#Given" ,"boundVariable v_v"),
    1.61 @@ -66,7 +66,7 @@
    1.62     rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
    1.63     scr=EmptyScr} : met),
    1.64  
    1.65 - (("DiffAppl.thy","make_fun_by_new_variable"):metID,
    1.66 + (("DiffAppl","make_fun_by_new_variable"):metID,
    1.67    {ppc = prep_met DiffAppl.thy
    1.68     [("#Given" ,"functionOf f_"),
    1.69      ("#Given" ,"boundVariable v_v"),
    1.70 @@ -76,7 +76,7 @@
    1.71     rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
    1.72     scr=EmptyScr} : met),
    1.73  
    1.74 - (("DiffAppl.thy","make_fun_by_explicit"):metID,
    1.75 + (("DiffAppl","make_fun_by_explicit"):metID,
    1.76    {ppc = prep_met DiffAppl.thy
    1.77     [("#Given" ,"functionOf f_"),
    1.78      ("#Given" ,"boundVariable v_v"),
    1.79 @@ -86,7 +86,7 @@
    1.80     rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
    1.81     scr=EmptyScr} : met),
    1.82    
    1.83 - (("DiffAppl.thy","max_on_interval_by_calculus"):metID,
    1.84 + (("DiffAppl","max_on_interval_by_calculus"):metID,
    1.85    {ppc = prep_met DiffAppl.thy
    1.86     [("#Given" ,"functionTerm t_"),
    1.87      ("#Given" ,"boundVariable v_v"),
    1.88 @@ -97,7 +97,7 @@
    1.89     rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
    1.90     scr=EmptyScr} : met),
    1.91  
    1.92 - (("DiffAppl.thy","find_values"):metID,
    1.93 + (("DiffAppl","find_values"):metID,
    1.94    {ppc = prep_met DiffAppl.thy
    1.95     [],
    1.96     rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],