Cl-isabelle-users August 2013 Archives by subject

• August 2013 messages sorted by: [ thread ] [ author ] [ date ]
• More info on this list...
• List archive Table of Contents

• Re: [isabelle] value "set [0,0::nat]" = "{0, 0}"::"nat set" – a bug?
  • Gottfried Barrow, gottfried.barrow@gmx.com - Fri, 30 Aug 2013 16:35:27 +0100
• Re: [isabelle] Formally proving the Boyer text matching algorithm
  • lyj238, lyj238@ios.ac.cn - Wed, 28 Aug 2013 00:37:11 +0100
• Re: [isabelle] "show" taking very long with goals with many hypothesis
  • Makarius, makarius@sketis.net - Wed, 07 Aug 2013 17:18:05 +0100
• [isabelle] value "set [0,0::nat]" = "{0, 0}"::"nat set" – a bug?
  • Christoph LANGE, math.semantic.web@gmail.com - Fri, 30 Aug 2013 16:13:37 +0100
• [isabelle] 2nd CFP Post-proceedings TYPES 2013 Types for Proofs and Programs (open call)
  • Aleksy Schubert, alx@mimuw.edu.pl - Thu, 08 Aug 2013 15:27:35 +0100
• Re: [isabelle] An easy (?) set comprehension lemma that should probably be in Set.thy
  • Lawrence Paulson, lp15@cam.ac.uk - Mon, 26 Aug 2013 11:58:51 +0100
  • Tobias Nipkow, nipkow@in.tum.de - Mon, 26 Aug 2013 13:32:29 +0100
• [isabelle] An easy (?) set comprehension lemma that should probably be in Set.thy
  • Christoph LANGE, math.semantic.web@gmail.com - Mon, 26 Aug 2013 11:52:08 +0100
• [isabelle] antiquotation for the current goal
  • Ondřej Kunčar, kuncar@in.tum.de - Fri, 23 Aug 2013 16:06:53 +0100
  • Makarius, makarius@sketis.net - Mon, 26 Aug 2013 10:35:38 +0100
  • Ondřej Kunčar, kuncar@in.tum.de - Mon, 26 Aug 2013 11:14:06 +0100
  • Makarius, makarius@sketis.net - Mon, 26 Aug 2013 11:29:19 +0100
• [isabelle] bit vs. bool in HOL-Word
  • Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de - Sun, 18 Aug 2013 15:36:08 +0100
  • Brian Huffman, huffman.brian.c@gmail.com - Sun, 18 Aug 2013 18:35:29 +0100
  • Thomas Sewell, Thomas.Sewell@nicta.com.au - Mon, 19 Aug 2013 02:13:33 +0100
  • Stefan Berghofer, berghofe@in.tum.de - Wed, 21 Aug 2013 16:55:58 +0100
  • Brian Huffman, huffman.brian.c@gmail.com - Wed, 21 Aug 2013 18:34:26 +0100
  • Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de - Tue, 27 Aug 2013 07:30:57 +0100
• [isabelle] Bitstrings as list of bools or ints
  • Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de - Sun, 18 Aug 2013 15:38:16 +0100
• [isabelle] Call for Papers: NFM 2014
  • Lawrence Paulson, lp15@cam.ac.uk - Sun, 11 Aug 2013 11:19:34 +0100
• [isabelle] Elbe Theory Viewer 1.67
  • Jens-D. Doll, jd@cococo.de - Fri, 23 Aug 2013 07:58:29 +0100
• [isabelle] FLoC 2014 Second Call for Workshops (The Sixth Federated Logic Conference, July 2014, Vienna)
  • Aleksy Schubert, alx@mimuw.edu.pl - Thu, 08 Aug 2013 16:28:06 +0100
• [isabelle] Formally proving the Boyer text matching algorithm
  • li yongjian, lyj238@gmail.com - Tue, 27 Aug 2013 16:06:56 +0100
  • Jasmin Blanchette, jasmin.blanchette@gmail.com - Tue, 27 Aug 2013 16:26:41 +0100
  • li yongjian, lyj238@gmail.com - Wed, 28 Aug 2013 00:08:19 +0100
  • Jasmin Blanchette, jasmin.blanchette@gmail.com - Wed, 28 Aug 2013 00:20:50 +0100
  • Lars Noschinski, noschinl@in.tum.de - Wed, 28 Aug 2013 14:59:03 +0100
• [isabelle] frequent jEdit crash (Mac OS10.8.4; Isabelle 2013)
  • Leo Freitas, leo.freitas@newcastle.ac.uk - Fri, 23 Aug 2013 15:14:23 +0100
  • Makarius, makarius@sketis.net - Mon, 26 Aug 2013 11:52:30 +0100
  • Tobias Nipkow, nipkow@in.tum.de - Mon, 26 Aug 2013 13:36:14 +0100
  • Makarius, makarius@sketis.net - Mon, 26 Aug 2013 13:58:02 +0100
  • Makarius, makarius@sketis.net - Mon, 26 Aug 2013 14:29:52 +0100
• Re: [isabelle] I need a meta-or
  • Gottfried Barrow, gottfried.barrow@gmx.com - Thu, 01 Aug 2013 02:05:40 +0100
  • Gottfried Barrow, gottfried.barrow@gmx.com - Thu, 01 Aug 2013 04:03:55 +0100
• [isabelle] install question
  • Peter Selinger, selinger@mathstat.dal.ca - Tue, 20 Aug 2013 00:49:39 +0100
  • Makarius, makarius@sketis.net - Mon, 26 Aug 2013 13:50:58 +0100
• [isabelle] jEdit - slowdown on split-view of same buffer
  • Palle Raabjerg, palle.raabjerg@it.uu.se - Fri, 23 Aug 2013 15:48:11 +0100
  • Makarius, makarius@sketis.net - Mon, 26 Aug 2013 13:36:15 +0100
• [isabelle] Kleene's Ternary Logic
  • Arthur Peters, amp@singingwizard.org - Mon, 26 Aug 2013 16:13:20 +0100
  • Jens-D. Doll, jd@cococo.de - Wed, 28 Aug 2013 07:37:54 +0100
  • Lawrence Paulson, lp15@cam.ac.uk - Wed, 28 Aug 2013 10:55:02 +0100
  • Jasmin Blanchette, jasmin.blanchette@gmail.com - Wed, 28 Aug 2013 11:29:14 +0100
• [isabelle] List.span
  • Christian Sternagel, c.sternagel@gmail.com - Tue, 13 Aug 2013 07:52:00 +0100
  • Tobias Nipkow, nipkow@in.tum.de - Wed, 14 Aug 2013 08:09:07 +0100
  • Christian Sternagel, c.sternagel@gmail.com - Wed, 14 Aug 2013 09:39:51 +0100
  • Makarius, makarius@sketis.net - Sat, 17 Aug 2013 18:25:13 +0100
• [isabelle] Localized Named Theorems
  • Christian Sternagel, c.sternagel@gmail.com - Wed, 28 Aug 2013 06:02:08 +0100
• [isabelle] match_tac, schematic and bound variables
  • Lars Noschinski, noschinl@in.tum.de - Mon, 12 Aug 2013 13:00:37 +0100
  • Makarius, makarius@sketis.net - Mon, 12 Aug 2013 17:14:02 +0100
  • Lawrence Paulson, lp15@cam.ac.uk - Mon, 12 Aug 2013 17:16:02 +0100
  • Tobias Nipkow, nipkow@in.tum.de - Mon, 12 Aug 2013 17:46:55 +0100
  • Makarius, makarius@sketis.net - Mon, 12 Aug 2013 19:10:02 +0100
  • Lawrence Paulson, lp15@cam.ac.uk - Mon, 12 Aug 2013 21:39:17 +0100
  • Tobias Nipkow, nipkow@in.tum.de - Tue, 13 Aug 2013 06:40:18 +0100
  • Lars Noschinski, noschinl@in.tum.de - Tue, 13 Aug 2013 10:34:55 +0100
  • Makarius, makarius@sketis.net - Sat, 17 Aug 2013 14:06:05 +0100
• [isabelle] MCS: Formal Proofs for Mathematics and Computer Science [Last Call for Papers]
  • Laurent Théry, Laurent.Thery@inria.fr - Thu, 22 Aug 2013 17:49:33 +0100
• [isabelle] nested datatypes
  • Jeremy Dawson, Jeremy.Dawson@anu.edu.au - Thu, 08 Aug 2013 05:18:47 +0100
  • Dmitriy Traytel, traytel@in.tum.de - Thu, 08 Aug 2013 11:34:20 +0100
• Re: [isabelle] nothing important
  • Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de - Sun, 04 Aug 2013 13:43:33 +0100
• [isabelle] one function for two datatypes
  • Henri DEBRAT, Henri.Debrat@loria.fr - Fri, 02 Aug 2013 22:21:29 +0100
  • Manuel Eberl, eberlm@in.tum.de - Sat, 03 Aug 2013 01:19:12 +0100
• Re: [isabelle] Ordinal of a datatype instantiated to enum
  • David Sanán, sananbad@scss.tcd.ie - Tue, 27 Aug 2013 15:08:33 +0100
  • David Sanán, sananbad@scss.tcd.ie - Tue, 27 Aug 2013 17:55:45 +0100
• Re: [isabelle] Questions about theories distributed with Isabelle
  • Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de - Sun, 04 Aug 2013 14:01:44 +0100
• [isabelle] Quotients of nominal types
  • Aleks Kissinger, aleks0@gmail.com - Wed, 07 Aug 2013 11:58:23 +0100
  • Christian Urban, christian.urban@kcl.ac.uk - Mon, 12 Aug 2013 08:38:54 +0100
  • Dmitriy Traytel, traytel@in.tum.de - Mon, 12 Aug 2013 09:25:56 +0100
  • Dmitriy Traytel, traytel@in.tum.de - Mon, 12 Aug 2013 09:40:55 +0100
  • Makarius, makarius@sketis.net - Mon, 12 Aug 2013 14:36:53 +0100
  • Christian Urban, christian.urban@kcl.ac.uk - Mon, 12 Aug 2013 15:22:28 +0100
  • Makarius, makarius@sketis.net - Mon, 12 Aug 2013 16:54:56 +0100
  • Aleks Kissinger, aleks0@gmail.com - Tue, 13 Aug 2013 14:23:28 +0100
• [isabelle] Regression with finite_Collect
  • René Neumann, rene.neumann@in.tum.de - Thu, 08 Aug 2013 12:18:30 +0100
• Re: [isabelle] Replacing COMP
  • René Neumann, rene.neumann@in.tum.de - Thu, 01 Aug 2013 09:36:16 +0100
  • René Neumann, rene.neumann@in.tum.de - Thu, 01 Aug 2013 09:43:39 +0100
  • René Neumann, rene.neumann@in.tum.de - Thu, 01 Aug 2013 09:45:52 +0100
  • Makarius, makarius@sketis.net - Thu, 01 Aug 2013 15:28:45 +0100
  • Makarius, makarius@sketis.net - Thu, 01 Aug 2013 15:34:39 +0100
  • Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de - Sun, 04 Aug 2013 18:19:42 +0100
  • René Neumann, rene.neumann@in.tum.de - Tue, 06 Aug 2013 13:00:28 +0100
• [isabelle] Research Fellow Position Birmingham
  • Manfred Kerber, mnfrd.krbr@gmail.com - Fri, 30 Aug 2013 12:09:14 +0100
• Re: [isabelle] Scala code generator: how to write code generated from Isabelle library dependencies to a shared package?
  • Christoph LANGE, math.semantic.web@gmail.com - Thu, 08 Aug 2013 15:47:45 +0100
• Re: [isabelle] Session with multiple parents
  • Makarius, makarius@sketis.net - Thu, 01 Aug 2013 16:33:16 +0100
• Re: [isabelle] string and altstring
  • Makarius, makarius@sketis.net - Sat, 17 Aug 2013 13:57:08 +0100
• [isabelle] subscripts in identifiers
  • Gergely Buday, gbuday@gmail.com - Thu, 22 Aug 2013 16:03:54 +0100
  • Gottfried Barrow, gottfried.barrow@gmx.com - Thu, 22 Aug 2013 17:43:26 +0100
• [isabelle] This is a Theorem (a song)
  • Joachim Breitner, breitner@kit.edu - Sun, 11 Aug 2013 21:31:12 +0100
• [isabelle] Trouble loading theories on windows
  • Jason Dagit, dagitj@gmail.com - Wed, 21 Aug 2013 07:00:46 +0100
  • Christian Sternagel, c.sternagel@gmail.com - Wed, 21 Aug 2013 08:09:57 +0100
  • Dominic Mulligan, dominic.p.mulligan@googlemail.com - Wed, 21 Aug 2013 09:45:15 +0100
  • Jason Dagit, dagitj@gmail.com - Wed, 21 Aug 2013 19:55:00 +0100
  • Jason Dagit, dagitj@gmail.com - Thu, 22 Aug 2013 18:56:59 +0100
• [isabelle] Which parser to use for theorems in a toplevel-command?
  • Lars Noschinski, noschinl@in.tum.de - Mon, 26 Aug 2013 10:12:56 +0100
  • Makarius, makarius@sketis.net - Mon, 26 Aug 2013 11:14:38 +0100
  • Lars Noschinski, noschinl@in.tum.de - Mon, 26 Aug 2013 14:46:36 +0100
  • Makarius, makarius@sketis.net - Mon, 26 Aug 2013 15:06:25 +0100