[isabelle-dev] Recent instabilities of HOL-Decision_Procs

[Florian Haftmann]

> The failure has now repeatly occured here:
> 
> *** Theory loader: undefined theory entry for "Approximation_Ex"
> *** Failed to finish proof
> *** At command "by" (line 42 of
> "/mnt/nfsbroy/home/isatest/isadist/Isabelle_04-Sep-2010/src/HOL/Decision_Procs/ex/Approximation_Ex.thy")
> 
> 
> i.e. this proof:
> 
> lemma "\<bar> exp 1.626 - 5.083499996273 \<bar> < (inverse 10 ^ 10 ::
> real)"
>   by (approximation 80)

Johannes and I have this problem on our screen (although we can not
pursue it actively at the moment due not yet available access to the
macbroy6 machine).

Our idea at the moment is to distill how we can reproduce the problem
and then inevitably trace the underlying code.

	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20100906/b4bf49f0/attachment.sig>