1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/isac/IsacKnowledge/LogExp.thy	Wed Jul 21 13:53:39 2010 +0200
     1.3 @@ -0,0 +1,30 @@
     1.4 +(* all outcommented in order to demonstrate authoring:
     1.5 +   WN071203
     1.6 +remove_thy"LogExp";
     1.7 +use_thy_only"IsacKnowledge/LogExp";
     1.8 +use_thy_only"IsacKnowledge/Isac";
     1.9 +*)
    1.10 +LogExp = PolyEq + 
    1.11 +
    1.12 +consts
    1.13 +
    1.14 +  ln     :: "real => real"
    1.15 +  exp    :: "real => real"         ("E'_ ^^^ _" 80)
    1.16 +
    1.17 +(*--------------------------------------------------*) 
    1.18 +  alog   :: "[real, real] => real" ("_ log _" 90)
    1.19 +
    1.20 +  (*Script-names*)
    1.21 +  Solve'_log    :: "[bool,real,        bool list] \
    1.22 +				   \=> bool list"
    1.23 +                  ("((Script Solve'_log (_ _=))//(_))" 9)
    1.24 +
    1.25 +rules
    1.26 +
    1.27 +  equality_pow    "0 < a ==> (l = r) = (a^^^l = a^^^r)"
    1.28 +  (* this is what students   ^^^^^^^... are told to do *)
    1.29 +  equality_power  "((a log b) = c) = (a^^^(a log b) = a^^^c)"
    1.30 +  exp_invers_log  "a^^^(a log b) = b"
    1.31 +(*---------------------------------------------------*)
    1.32 +
    1.33 +end
    1.34 \ No newline at end of file