1.1 --- a/src/Tools/isac/IsacKnowledge/LogExp.ML	Wed Aug 25 15:15:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,39 +0,0 @@
     1.4 -(* all outcommented in order to demonstrate authoring:
     1.5 -   WN071203
     1.6 -*)
     1.7 -
     1.8 -(** interface isabelle -- isac **)
     1.9 -theory' := overwritel (!theory', [("LogExp.thy",LogExp.thy)]);
    1.10 -
    1.11 -(*--------------------------------------------------*)
    1.12 -
    1.13 -(** problems **)
    1.14 -store_pbt
    1.15 - (prep_pbt LogExp.thy "pbl_test_equ_univ_log" [] e_pblID
    1.16 - (["logarithmic","univariate","equation"],
    1.17 -  [("#Given",["equality e_","solveFor v_"]),
    1.18 -   ("#Where",["matches ((?a log ?v_) = ?b) e_"]),
    1.19 -   ("#Find" ,["solutions v_i_"]),
    1.20 -   ("#With" ,["||(lhs (Subst (v_i_,v_) e_) - \
    1.21 -	      \  (rhs (Subst (v_i_,v_) e_) || < eps)"])
    1.22 -   ],
    1.23 -  PolyEq_prls, SOME "solve (e_::bool, v_)",
    1.24 -  [["Equation","solve_log"]]));
    1.25 -
    1.26 -(** methods **)
    1.27 -store_met
    1.28 - (prep_met LogExp.thy "met_equ_log" [] e_metID
    1.29 - (["Equation","solve_log"],
    1.30 -  [("#Given" ,["equality e_","solveFor v_"]),
    1.31 -   ("#Where" ,["matches ((?a log ?v_) = ?b) e_"]),
    1.32 -   ("#Find"  ,["solutions v_i_"])
    1.33 -  ],
    1.34 -   {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
    1.35 -    calc=[],crls=PolyEq_crls, nrls=norm_Rational},
    1.36 -    "Script Solve_log (e_::bool) (v_::real) =     \
    1.37 -    \(let e_ = ((Rewrite equality_power False) @@ \
    1.38 -    \           (Rewrite exp_invers_log False) @@ \
    1.39 -    \           (Rewrite_Set norm_Poly False)) e_ \
    1.40 -    \ in [e_])"
    1.41 -   ));
    1.42 -(*--------------------------------------------------*)