1.1 --- a/src/sml/IsacKnowledge/LogExp.ML	Mon Dec 03 19:11:27 2007 +0100
     1.2 +++ b/src/sml/IsacKnowledge/LogExp.ML	Mon Dec 03 19:45:05 2007 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4     ("#Find"  ,["solutions v_i_"])
     1.5     ],
     1.6    PolyEq_prls, Some "solve (e_::bool, v_)",
     1.7 -  [["Test","solve_log"]]));
     1.8 +  [["Equation","solve_log"]]));
     1.9  
    1.10  (** methods **)
    1.11  store_met

     2.1 --- a/src/sml/IsacKnowledge/LogExp.thy	Mon Dec 03 19:11:27 2007 +0100
     2.2 +++ b/src/sml/IsacKnowledge/LogExp.thy	Mon Dec 03 19:45:05 2007 +0100
     2.3 @@ -1,12 +1,12 @@
     2.4  (* all outcommented in order to demonstrate authoring:
     2.5     WN071203
     2.6  remove_thy"LogExp";
     2.7 -use_thy"IsacKnowledge/LogExp";
     2.8 +use_thy_only"IsacKnowledge/LogExp";
     2.9  use_thy"IsacKnowledge/Isac";
    2.10  *)
    2.11  LogExp = PolyEq + 
    2.12  
    2.13 -(*----------------------------------------------------------*
    2.14 +(*----------------------------------------------------------*)
    2.15  consts
    2.16  
    2.17    ln     :: "real => real"
    2.18 @@ -23,6 +23,6 @@
    2.19    equality_pow    "0 < a ==> (l = r) = (a^^^l = a^^^r)"
    2.20    equality_power  "((a log b) = c) = (a^^^(a log b) = a^^^c)"
    2.21    exp_invers_log  "a^^^(a log b) = b"
    2.22 -*----------------------------------------------------------*)
    2.23 +(*----------------------------------------------------------*)
    2.24  
    2.25  end
    2.26 \ No newline at end of file