1.1 --- a/src/sml/IsacKnowledge/Diff.thy	Sat Nov 24 18:59:07 2007 +0100
     1.2 +++ b/src/sml/IsacKnowledge/Diff.thy	Mon Dec 03 15:54:09 2007 +0100
     1.3 @@ -13,10 +13,6 @@
     1.4  
     1.5    d_d           :: "[real, real]=> real"
     1.6    sin, cos      :: "real => real"
     1.7 -  log, ln       :: "real => real"
     1.8 -  nlog          :: "[real, real] => real"
     1.9 -  exp           :: "real => real"         ("E'_ ^^^ _" 80)
    1.10 -
    1.11    (*descriptions in the related problems*)
    1.12    derivativeEq  :: bool => una
    1.13  

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/sml/IsacKnowledge/LogExp.thy	Mon Dec 03 15:54:09 2007 +0100
     2.3 @@ -0,0 +1,13 @@
     2.4 +(* all outcommented for demonstrating authoring:
     2.5 +   WN071203
     2.6 +*)
     2.7 +LogExp = Real +
     2.8 +
     2.9 +(*----------------------------------------------------------*)
    2.10 +consts
    2.11 +
    2.12 +  ln     :: "real => real"
    2.13 +  alog   :: "[real, real] => real" ("_ log _" 80)
    2.14 +  exp    :: "real => real"         ("E'_ ^^^ _" 80)
    2.15 +
    2.16 +end
    2.17 \ No newline at end of file