(* all outcommented in order to demonstrate authoring:

    WN071203

 remove_thy"LogExp";

 use_thy_only"IsacKnowledge/LogExp";

 use_thy_only"IsacKnowledge/Isac";

 *)

 LogExp = PolyEq + 

 consts

   ln     :: "real => real"

   exp    :: "real => real"         ("E'_ ^^^ _" 80)

 (*----------------------------------------------------------*

   alog   :: "[real, real] => real" ("_ log _" 90)

   (*Script-names*)

   Solve'_log    :: "[bool,real,        bool list] \

 				   \=> bool list"

                   ("((Script Solve'_log (_ _=))// (_))" 9)

 rules

   equality_pow    "0 < a ==> (l = r) = (a^^^l = a^^^r)"

   equality_power  "((a log b) = c) = (a^^^(a log b) = a^^^c)"

   exp_invers_log  "a^^^(a log b) = b"

 *----------------------------------------------------------*)

 end