1.1 --- a/src/sml/IsacKnowledge/Biegelinie.ML	Thu Feb 21 16:48:59 2008 +0100
     1.2 +++ b/src/sml/IsacKnowledge/Biegelinie.ML	Thu Feb 21 17:09:19 2008 +0100
     1.3 @@ -439,17 +439,6 @@
     1.4  ));
     1.5  
     1.6  store_met
     1.7 -    (prep_met Biegelinie.thy "met_equ" [] e_metID
     1.8 -	      (["Equation"],
     1.9 -	       [],
    1.10 -	       {rew_ord'="tless_true", rls'=Erls, calc = [], 
    1.11 -		srls = e_rls, 
    1.12 -		prls=e_rls,
    1.13 -	     crls = Atools_erls, nrls = e_rls},
    1.14 -"empty_script"
    1.15 -));
    1.16 -
    1.17 -store_met
    1.18      (prep_met Biegelinie.thy "met_equ_fromfun" [] e_metID
    1.19  	      (["Equation","fromFunction"],
    1.20  	       [("#Given" ,["functionEq fun_","substitution sub_"]),

     2.1 --- a/src/sml/IsacKnowledge/Equation.ML	Thu Feb 21 16:48:59 2008 +0100
     2.2 +++ b/src/sml/IsacKnowledge/Equation.ML	Thu Feb 21 17:09:19 2008 +0100
     2.3 @@ -70,3 +70,16 @@
     2.4  	       argl2dtss))
     2.5  	     ]);
     2.6  
     2.7 +
     2.8 +
     2.9 +store_met
    2.10 +    (prep_met Equation.thy "met_equ" [] e_metID
    2.11 +	      (["Equation"],
    2.12 +	       [],
    2.13 +	       {rew_ord'="tless_true", rls'=Erls, calc = [], 
    2.14 +		srls = e_rls, 
    2.15 +		prls=e_rls,
    2.16 +	     crls = Atools_erls, nrls = e_rls},
    2.17 +"empty_script"
    2.18 +));
    2.19 +

     3.1 --- a/src/sml/IsacKnowledge/Isac.thy	Thu Feb 21 16:48:59 2008 +0100
     3.2 +++ b/src/sml/IsacKnowledge/Isac.thy	Thu Feb 21 17:09:19 2008 +0100
     3.3 @@ -2,7 +2,7 @@
     3.4     WN.11.00
     3.5   *)
     3.6  
     3.7 -Isac = PolyMinus + Equation + PolyEq + Vect + DiffApp + Biegelinie + AlgEin
     3.8 +Isac = PolyMinus + PolyEq + Vect + DiffApp + Biegelinie + AlgEin
     3.9         + (*InsSort +*) Test + 
    3.10  
    3.11  end

     4.1 --- a/src/sml/IsacKnowledge/LinEq.thy	Thu Feb 21 16:48:59 2008 +0100
     4.2 +++ b/src/sml/IsacKnowledge/LinEq.thy	Thu Feb 21 17:09:19 2008 +0100
     4.3 @@ -16,7 +16,7 @@
     4.4  
     4.5  *)
     4.6  
     4.7 -LinEq = Poly + 
     4.8 +LinEq = Poly + Equation +
     4.9  
    4.10  (*-------------------- consts------------------------------------------------*)
    4.11  consts

     5.1 --- a/src/sml/IsacKnowledge/LogExp.ML	Thu Feb 21 16:48:59 2008 +0100
     5.2 +++ b/src/sml/IsacKnowledge/LogExp.ML	Thu Feb 21 17:09:19 2008 +0100
     5.3 @@ -5,15 +5,17 @@
     5.4  (** interface isabelle -- isac **)
     5.5  theory' := overwritel (!theory', [("LogExp.thy",LogExp.thy)]);
     5.6  
     5.7 -(*-------------------------------------------------------------------*
     5.8 +(*--------------------------------------------------*)
     5.9  
    5.10  (** problems **)
    5.11  store_pbt
    5.12   (prep_pbt LogExp.thy "pbl_test_equ_univ_log" [] e_pblID
    5.13   (["logarithmic","univariate","equation"],
    5.14 -  [("#Given" ,["equality e_","solveFor v_"]),
    5.15 -   ("#Where" ,["matches ((?a log ?v_) = ?b) e_"]),
    5.16 -   ("#Find"  ,["solutions v_i_"])
    5.17 +  [("#Given",["equality e_","solveFor v_"]),
    5.18 +   ("#Where",["matches ((?a log ?v_) = ?b) e_"]),
    5.19 +   ("#Find" ,["solutions v_i_"]),
    5.20 +   ("#With" ,["||(lhs (Subst (v_i_,v_) e_) - \
    5.21 +	      \  (rhs (Subst (v_i_,v_) e_) || < eps)"])
    5.22     ],
    5.23    PolyEq_prls, Some "solve (e_::bool, v_)",
    5.24    [["Equation","solve_log"]]));
    5.25 @@ -34,4 +36,4 @@
    5.26      \           (Rewrite_Set norm_Poly False)) e_ \
    5.27      \ in [e_])"
    5.28     ));
    5.29 -*-------------------------------------------------------------------*)
    5.30 +(*--------------------------------------------------*)

     6.1 --- a/src/sml/IsacKnowledge/LogExp.thy	Thu Feb 21 16:48:59 2008 +0100
     6.2 +++ b/src/sml/IsacKnowledge/LogExp.thy	Thu Feb 21 17:09:19 2008 +0100
     6.3 @@ -11,19 +11,19 @@
     6.4    ln     :: "real => real"
     6.5    exp    :: "real => real"         ("E'_ ^^^ _" 80)
     6.6  
     6.7 -(*----------------------------------------------------------*
     6.8 +(*--------------------------------------------------*)
     6.9    alog   :: "[real, real] => real" ("_ log _" 90)
    6.10  
    6.11    (*Script-names*)
    6.12    Solve'_log    :: "[bool,real,        bool list] \
    6.13  				   \=> bool list"
    6.14 -                  ("((Script Solve'_log (_ _=))// (_))" 9)
    6.15 +                  ("((Script Solve'_log (_ _=))//(_))" 9)
    6.16  
    6.17  rules
    6.18  
    6.19    equality_pow    "0 < a ==> (l = r) = (a^^^l = a^^^r)"
    6.20    equality_power  "((a log b) = c) = (a^^^(a log b) = a^^^c)"
    6.21    exp_invers_log  "a^^^(a log b) = b"
    6.22 -*----------------------------------------------------------*)
    6.23 +(*---------------------------------------------------*)
    6.24  
    6.25  end
    6.26 \ No newline at end of file