1.1 --- a/src/sml/IsacKnowledge/Atools.thy	Thu May 10 11:06:34 2007 +0200
     1.2 +++ b/src/sml/IsacKnowledge/Atools.thy	Thu May 10 11:06:34 2007 +0200
     1.3 @@ -39,10 +39,12 @@
     1.4    (* identity on term level*)
     1.5    "ident"     :: ['a, 'a] => bool    ("(_ =!=/ _)" [51, 51] 50)
     1.6  
     1.7 -  "argument'_in"  :: real => real ("argument'_in _" 10)
     1.8 -  "sameFunId"     :: [real, bool] => bool (**"same'_funid _ _" 10
     1.9 +  "argument'_in"    :: real => real ("argument'_in _" 10)
    1.10 +  "sameFunId"       :: [real, bool] => bool (**"same'_funid _ _" 10
    1.11  	WN0609 changed the id, because ".. _ _" inhibits currying**)
    1.12 -  "boollist2sum"  :: bool list => real
    1.13 +  "filter'_sameFunId":: [real, bool list] => real list 
    1.14 +					("filter'_sameFunId _ _" 10)
    1.15 +  "boollist2sum"    :: bool list => real
    1.16  
    1.17  (*-------------------- rules -------------------------------------*)
    1.18  rules (*for evaluating the assumptions of conditional rules*)

     2.1 --- a/src/sml/IsacKnowledge/Biegelinie.ML	Thu May 10 11:06:34 2007 +0200
     2.2 +++ b/src/sml/IsacKnowledge/Biegelinie.ML	Thu May 10 11:06:34 2007 +0200
     2.3 @@ -407,6 +407,33 @@
     2.4  \                          [Equation,fromFunction])              \
     2.5  \                          [bool_ (hd fs_), bool_ b4_])          \
     2.6  \ in [e1_,e2_,e3_,e4_])"
     2.7 +(* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
     2.8 +"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \
     2.9 +\ (let b1_ = nth_ 1 rb_;                                         \
    2.10 +\      fs_ = filter (sameFunId (lhs b1_)) funs_;                 \
    2.11 +\      (e1_::bool) =                                             \
    2.12 +\             (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
    2.13 +\                          [Equation,fromFunction])              \
    2.14 +\                          [bool_ (hd fs_), bool_ b1_]);         \
    2.15 +\      b2_ = nth_ 2 rb_;                                         \
    2.16 +\      fs_ = filter (sameFunId (lhs b2_)) funs_;                 \
    2.17 +\      (e2_::bool) =                                             \
    2.18 +\             (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
    2.19 +\                          [Equation,fromFunction])              \
    2.20 +\                          [bool_ (hd fs_), bool_ b2_]);         \
    2.21 +\      b3_ = nth_ 3 rb_;                                         \
    2.22 +\      fs_ = filter (sameFunId (lhs b3_)) funs_;                 \
    2.23 +\      (e3_::bool) =                                             \
    2.24 +\             (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
    2.25 +\                          [Equation,fromFunction])              \
    2.26 +\                          [bool_ (hd fs_), bool_ b3_]);         \
    2.27 +\      b4_ = nth_ 4 rb_;                                         \
    2.28 +\      fs_ = filter (sameFunId (lhs b4_)) funs_;                 \
    2.29 +\      (e4_::bool) =                                             \
    2.30 +\             (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
    2.31 +\                          [Equation,fromFunction])              \
    2.32 +\                          [bool_ (hd fs_), bool_ b4_])          \
    2.33 +\ in [e1_,e2_,e3_,e4_])"*)
    2.34  ));
    2.35  
    2.36  store_met