Cl-isabelle-users August 2013 Archives by subject
- Re: [isabelle] value "set [0,0::nat]" = "{0, 0}"::"nat set" – a bug?
- 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)
- Re: [isabelle] An easy (?) set comprehension lemma that should probably be in Set.thy
- [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
- [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)
- [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
- [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
- [isabelle] List.span
- [isabelle] Localized Named Theorems
- [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
- [isabelle] This is a Theorem (a song)
- [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
This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.