<table cellspacing="0" cellpadding="0" border="0" ><tr><td valign="top" style="font: inherit;"><DIV>I was wondering if anyone has verified the CAN or controller area network using ISABELLE  ??</DIV>
<DIV> </DIV>
<DIV>David</DIV>
<DIV> </DIV>
<DIV> </DIV>
<DIV><BR><BR>--- On <B>Mon, 4/30/12, isabelle-dev-request@mailbroy.informatik.tu-muenchen.de <I><isabelle-dev-request@mailbroy.informatik.tu-muenchen.de></I></B> wrote:<BR></DIV>
<BLOCKQUOTE style="BORDER-LEFT: rgb(16,16,255) 2px solid; PADDING-LEFT: 5px; MARGIN-LEFT: 5px"><BR>From: isabelle-dev-request@mailbroy.informatik.tu-muenchen.de <isabelle-dev-request@mailbroy.informatik.tu-muenchen.de><BR>Subject: isabelle-dev Digest, Vol 59, Issue 52<BR>To: isabelle-dev@mailbroy.informatik.tu-muenchen.de<BR>Date: Monday, April 30, 2012, 6:00 AM<BR><BR>
<DIV class=plainMail>Send isabelle-dev mailing list submissions to<BR>    <A href="http://us.mc1133.mail.yahoo.com/mc/compose?to=isabelle-dev@mailbroy.informatik.tu-muenchen.de" ymailto="mailto:isabelle-dev@mailbroy.informatik.tu-muenchen.de">isabelle-dev@mailbroy.informatik.tu-muenchen.de</A><BR><BR>To subscribe or unsubscribe via the World Wide Web, visit<BR>    <A href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev" target=_blank>https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</A><BR><BR>or, via email, send a message with subject or body 'help' to<BR>    <A href="http://us.mc1133.mail.yahoo.com/mc/compose?to=isabelle-dev-request@mailbroy.informatik.tu-muenchen.de" ymailto="mailto:isabelle-dev-request@mailbroy.informatik.tu-muenchen.de">isabelle-dev-request@mailbroy.informatik.tu-muenchen.de</A><BR><BR>You can reach the person managing the list
 at<BR>    <A href="http://us.mc1133.mail.yahoo.com/mc/compose?to=isabelle-dev-owner@mailbroy.informatik.tu-muenchen.de" ymailto="mailto:isabelle-dev-owner@mailbroy.informatik.tu-muenchen.de">isabelle-dev-owner@mailbroy.informatik.tu-muenchen.de</A><BR><BR>When replying, please edit your Subject line so it is more specific<BR>than "Re: Contents of isabelle-dev digest..."<BR><BR><BR>Today's Topics:<BR><BR>   1. Alternative approach to ?efficient? natural numbers<BR>      (Florian Haftmann)<BR>   2. Re: Isabelle release test website (Makarius)<BR>   3. Haskabelle update? (Makarius)<BR><BR><BR>----------------------------------------------------------------------<BR><BR>Message: 1<BR>Date: Sun, 29 Apr 2012 15:51:26 +0200<BR>From: Florian Haftmann <<A href="http://us.mc1133.mail.yahoo.com/mc/compose?to=florian.haftmann@informatik.tu-muenchen.de"
 ymailto="mailto:florian.haftmann@informatik.tu-muenchen.de">florian.haftmann@informatik.tu-muenchen.de</A>><BR>To: DEV Isabelle Mailinglist <<A href="http://us.mc1133.mail.yahoo.com/mc/compose?to=isabelle-dev@in.tum.de" ymailto="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</A>><BR>Subject: [isabelle-dev] Alternative approach to ?efficient? natural<BR>    numbers<BR>Message-ID: <<A href="http://us.mc1133.mail.yahoo.com/mc/compose?to=4F9D475E.5030108@informatik.tu-muenchen.de" ymailto="mailto:4F9D475E.5030108@informatik.tu-muenchen.de">4F9D475E.5030108@informatik.tu-muenchen.de</A>><BR>Content-Type: text/plain; charset="iso-8859-15"<BR><BR>Hi all,<BR><BR>I did an experiment with Flyspeck-Tame (on macbroyXY):<BR><BR>Using the Efficient_Nat theory where Isabelle nat is directly<BR>represented as PolyML int:<BR><BR>> Finished HOL-Flyspeck-Tame (11:50:46 elapsed time, 13:54:35 cpu time, factor 1.17)<BR><BR>Using the
 Target_Numeral theory where Isabelle nat is an abstract<BR>datatype over PolyML int:<BR><BR>> Finished HOL-Flyspeck-Tame (10:55:49 elapsed time, 13:57:31 cpu time, factor 1.27)<BR><BR>The reason why this has the same magnitude of runtime is that in PolyML<BR>trivial datatypes like<BR><BR>> datatype nat = Nat of int<BR>> fun int_of (Nat k) = k<BR><BR>are optimized away.<BR><BR>This is a proof of concept that it is possible in the future to have<BR>just *one* type which is mapped onto target language numerals by<BR>default, and to refine nat and/or int to use this is implementation if<BR>desired, rather than adhoc code_const setups etc. for nat and int.  Cf.<BR>also <A href="https://isabelle.in.tum.de/community/Numerals" target=_blank>https://isabelle.in.tum.de/community/Numerals</A><BR><BR>Cheers,<BR>    Florian<BR><BR>P.S. This his no consequences for the upcoming release.<BR><BR>-- <BR><BR>PGP available:<BR><A
 href="http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de" target=_blank>http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de</A><BR><BR>-------------- next part --------------<BR>A non-text attachment was scrubbed...<BR>Name: signature.asc<BR>Type: application/pgp-signature<BR>Size: 262 bytes<BR>Desc: OpenPGP digital signature<BR>URL: <<A href="https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120429/b9c957c6/attachment-0001.asc" target=_blank>https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120429/b9c957c6/attachment-0001.asc</A>><BR><BR>------------------------------<BR><BR>Message: 2<BR>Date: Sun, 29 Apr 2012 16:35:02 +0200 (CEST)<BR>From: Makarius <<A href="http://us.mc1133.mail.yahoo.com/mc/compose?to=makarius@sketis.net"
 ymailto="mailto:makarius@sketis.net">makarius@sketis.net</A>><BR>To: <A href="http://us.mc1133.mail.yahoo.com/mc/compose?to=isabelle-dev@mailbroy.informatik.tu-muenchen.de" ymailto="mailto:isabelle-dev@mailbroy.informatik.tu-muenchen.de">isabelle-dev@mailbroy.informatik.tu-muenchen.de</A><BR>Subject: Re: [isabelle-dev] Isabelle release test website<BR>Message-ID:<BR>    <<A href="http://us.mc1133.mail.yahoo.com/mc/compose?to=alpine.LNX.2.00.1204291629510.19214@macbroy21.informatik.tu-muenchen.de" ymailto="mailto:alpine.LNX.2.00.1204291629510.19214@macbroy21.informatik.tu-muenchen.de">alpine.LNX.2.00.1204291629510.19214@macbroy21.informatik.tu-muenchen.de</A>><BR>    <BR>Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed<BR><BR>This is probably the last update of the test website <BR><A href="http://www4.in.tum.de/~wenzelm/test/website/" target=_blank>http://www4.in.tum.de/~wenzelm/test/website/</A> before
 official release <BR>candidates for Isabelle2012 will be announced (also on isabelle-users).<BR><BR>The current plan for the deadline for point 0 (the repository fork) is <BR>02-May-2012 -- I will announce it again to make sure that no changeset <BR>gets in the wrong place in the critical moment.<BR><BR>Afterwards any important amendments need to be sent as individual <BR>changesets to me via email.<BR><BR><BR>    Makarius<BR><BR><BR>------------------------------<BR><BR>Message: 3<BR>Date: Sun, 29 Apr 2012 16:51:04 +0200 (CEST)<BR>From: Makarius <<A href="http://us.mc1133.mail.yahoo.com/mc/compose?to=makarius@sketis.net" ymailto="mailto:makarius@sketis.net">makarius@sketis.net</A>><BR>To: <A href="http://us.mc1133.mail.yahoo.com/mc/compose?to=isabelle-dev@in.tum.de" ymailto="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</A><BR>Subject: [isabelle-dev] Haskabelle update?<BR>Message-ID:<BR>    <<A
 href="http://us.mc1133.mail.yahoo.com/mc/compose?to=alpine.LNX.2.00.1204291650040.19709@macbroy21.informatik.tu-muenchen.de" ymailto="mailto:alpine.LNX.2.00.1204291650040.19709@macbroy21.informatik.tu-muenchen.de">alpine.LNX.2.00.1204291650040.19709@macbroy21.informatik.tu-muenchen.de</A>><BR>    <BR>Content-Type: TEXT/PLAIN; format=flowed; charset=US-ASCII<BR><BR>Who is maintaining Haskabelle?  Are there plans to update it for the <BR>coming release?<BR><BR>So far I have bundled Haskabelle2011-1.tar.gz from last time.<BR><BR><BR>    Makarius<BR><BR><BR>------------------------------<BR><BR>_______________________________________________<BR>isabelle-dev mailing list<BR><A href="http://us.mc1133.mail.yahoo.com/mc/compose?to=isabelle-dev@mailbroy.informatik.tu-muenchen.de" ymailto="mailto:isabelle-dev@mailbroy.informatik.tu-muenchen.de">isabelle-dev@mailbroy.informatik.tu-muenchen.de</A><BR><A
 href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev" target=_blank>https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</A><BR><BR><BR>End of isabelle-dev Digest, Vol 59, Issue 52<BR>********************************************<BR></DIV></BLOCKQUOTE></td></tr></table>