1.1 --- a/src/Tools/isac/Knowledge/LogExp.thy	Sat Jun 22 13:15:52 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy	Sat Jun 22 14:34:06 2019 +0200
     1.3 @@ -8,15 +8,8 @@
     1.4  
     1.5    ln     :: "real => real"
     1.6    exp    :: "real => real"         ("E'_ ^^^ _" 80)
     1.7 -
     1.8 -(*--------------------------------------------------*) 
     1.9    alog   :: "[real, real] => real" ("_ log _" 90)
    1.10  
    1.11 -  (*Script-names*)
    1.12 -  Solve'_log    :: "[bool,real,        bool list]  
    1.13 -				    => bool list"
    1.14 -                  ("((Script Solve'_log (_ _=))//(_))" 9)
    1.15 -
    1.16  axiomatization where
    1.17  
    1.18    equality_pow:    "0 < a ==> (l = r) = (a^^^l = a^^^r)" and
    1.19 @@ -55,12 +48,7 @@
    1.20            ("#Find"  ,["solutions v_v'i'"])],
    1.21          {rew_ord' = "termlessI", rls' = PolyEq_erls, srls = Rule.e_rls, prls = PolyEq_prls, calc = [],
    1.22            crls = PolyEq_crls, errpats = [], nrls = norm_Rational},
    1.23 -        @{thm solve_log.simps}
    1.24 -	    (*"Script Solve_log (e_e::bool) (v_v::real) =     " ^
    1.25 -        "(let e_e = ((Rewrite ''equality_power'' False) @@ " ^
    1.26 -        "           (Rewrite ''exp_invers_log'' False) @@  " ^
    1.27 -        "           (Rewrite_Set ''norm_Poly'' False)) e_e " ^
    1.28 -        " in [e_e])"*))]
    1.29 +        @{thm solve_log.simps})]
    1.30  \<close>
    1.31  
    1.32  end
    1.33 \ No newline at end of file