(* 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)"

   (* this is what students   ^^^^^^^... are told to do *)

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

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

 (*---------------------------------------------------*)

 end