On 21.11.2013, at 10:56 pm, Makarius wrote:
>> Did anybody test WWW_Find?
Have just confirmed that WWW_Find works fine with Isabelle2013-2-RC2
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal
professional privilege and/o
Important note: isatest is presently testing
https://bitbucket.org/isabelle_project/isabelle-release again.
There have been a bit too many posthoc changes for Isabelle2013-1 to trust
blindly that the usual collection of isatest platforms still work. The
final Isabelle2013-2 release will probab
Hi Florian,
> Just a remark on
> http://isabelle.in.tum.de/repos/isabelle/rev/8c0a27b9c1bd: the matter on
> lexicographic orderings in List.thy is now numerous enough but still
> self-contained to justify a separate theory Lexorder.thy.
I agree that a separate theory would be nice. But before do
Hi Florian,
a) Char_ord and List_lexord are not tied together, i.e., a user could
import List_lexord, but not Char_ord, define his own version of order on
String.literal and the generated Haskell code compiles, but it is
unsound (even without any further adaptations by the user). One could
solve
Just a remark on
http://isabelle.in.tum.de/repos/isabelle/rev/8c0a27b9c1bd: the matter on
lexicographic orderings in List.thy is now numerous enough but still
self-contained to justify a separate theory Lexorder.thy. I would also
suggest that the predicate version should be done using locales rath
Hi Andreas & René,
> a) Char_ord and List_lexord are not tied together, i.e., a user could
> import List_lexord, but not Char_ord, define his own version of order on
> String.literal and the generated Haskell code compiles, but it is
> unsound (even without any further adaptations by the user). On
Just for the record: I have resolved that issue as shown in
63fe59f64578. See also 0e6645622f22 for a related issue.
Florian
Am 19.09.2013 19:05, schrieb Florian Haftmann:
> Since, there 92080294beb8 are two clone theories:
>
> Library/Univ_Poly.thy
> Decision_Procs/Polynom
