1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Wed Aug 25 16:20:07 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"Knowledge/LogExp";
1.8 +use_thy_only"Knowledge/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