1.1 --- a/src/Tools/isac/IsacKnowledge/LogExp.thy	Wed Aug 25 15:15:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,30 +0,0 @@
     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