Cl-isabelle-users December 2013 Archives by date

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

• Sun, 01 Dec 2013
  • Re: [isabelle] Isabelle2013-2-RC2 available for testing - bnord, bnord01@gmail.com
  • Re: [isabelle] Isabelle2013-2-RC2 available for testing - Makarius, makarius@sketis.net
  • Re: [isabelle] Knaster-Tarski Lemma - Makarius, makarius@sketis.net
  • Re: [isabelle] Knaster-Tarski Lemma - Alfio Martini, alfio.martini@acm.org
  • [isabelle] Isabelle2013-2-RC3 available for testing - Makarius, makarius@sketis.net
  • Re: [isabelle] Isabelle2013-2-RC3 available for testing - Makarius, makarius@sketis.net
  • Re: [isabelle] Window title and icon of Isabelle/jEdit says "jEdit" - Makarius, makarius@sketis.net
  • Re: [isabelle] feature request: defining tuples - Konrad Slind, konrad.slind@gmail.com
  • Re: [isabelle] Isabelle2013-2-RC2 available for testing - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] Stray processes on Windows - Makarius, makarius@sketis.net
  • Re: [isabelle] Isabelle2013-2-RC2 available for testing - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • [isabelle] Non-atomic premise - Joachim Breitner, breitner@kit.edu
• Mon, 02 Dec 2013
  • Re: [isabelle] Non-atomic premise - Brian Huffman, huffman.brian.c@gmail.com
  • [isabelle] comm_monoid_big not in Isabelle 2013-1 - Andrew Boyton, Andrew.Boyton@nicta.com.au
  • [isabelle] Underscore vs Hyphen in Document Preparation - Alfio Martini, alfio.martini@acm.org
  • Re: [isabelle] Isabelle2013-2-RC2 available for testing - bnord, bnord01@gmail.com
  • [isabelle] AI4FM 2014: Call for Short Contributions - Iain Whiteside, Iain.Whiteside@newcastle.ac.uk
  • Re: [isabelle] comm_monoid_big not in Isabelle 2013-1 - Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de
  • Re: [isabelle] Underscore vs Hyphen in Document Preparation - Makarius, makarius@sketis.net
  • Re: [isabelle] Isabelle2013-2-RC2 available for testing - Makarius, makarius@sketis.net
  • [isabelle] Line numbers vs. icons - Makarius, makarius@sketis.net
  • Re: [isabelle] Stray processes on Windows - Makarius, makarius@sketis.net
  • [isabelle] Default print modes - Peter Lammich, lammich@in.tum.de
  • [isabelle] Error when Importing Theories from Library - Alfio Martini, alfio.martini@acm.org
  • Re: [isabelle] Isabelle2013-2-RC2 available for testing - Makarius, makarius@sketis.net
  • Re: [isabelle] Isabelle2013-2-RC2 available for testing - Makarius, makarius@sketis.net
  • Re: [isabelle] Isabelle2013-2-RC2 available for testing - Makarius, makarius@sketis.net
  • Re: [isabelle] Line numbers vs. icons - Gottfried Barrow, gottfried.barrow@gmx.com
  • Re: [isabelle] Error when Importing Theories from Library - Makarius, makarius@sketis.net
  • Re: [isabelle] Default print modes - Makarius, makarius@sketis.net
  • Re: [isabelle] Line numbers vs. icons - Makarius, makarius@sketis.net
  • Re: [isabelle] feature request: defining tuples - Makarius, makarius@sketis.net
  • Re: [isabelle] feature request: defining tuples - John Wickerson, johnwickerson@cantab.net
  • Re: [isabelle] feature request: defining tuples - Makarius, makarius@sketis.net
  • Re: [isabelle] Line numbers vs. icons - Gottfried Barrow, gottfried.barrow@gmx.com
  • Re: [isabelle] export_code doesn't define Trueprop for False - Gottfried Barrow, gottfried.barrow@gmx.com
• Tue, 03 Dec 2013
  • Re: [isabelle] Underscore vs Hyphen in Document Preparation - Tobias Nipkow, nipkow@in.tum.de
  • [isabelle] LaTeXsygar (bug or feature?) - Alfio Martini, alfio.martini@acm.org
  • Re: [isabelle] LaTeXsygar (bug or feature?) - Gerwin Klein, Gerwin.Klein@nicta.com.au
  • Re: [isabelle] LaTeXsygar (bug or feature?) - Alfio Martini, alfio.martini@acm.org
  • [isabelle] exception using "case ... of ..." with HOLCF - Christian Sternagel, c.sternagel@gmail.com
  • [isabelle] Casting records efficiently - René Neumann, rene.neumann@in.tum.de
  • Re: [isabelle] Casting records efficiently - René Neumann, rene.neumann@in.tum.de
  • Re: [isabelle] Knaster-Tarski Lemma - Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de
  • Re: [isabelle] Casting records efficiently - Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de
  • Re: [isabelle] Casting records efficiently - René Neumann, rene.neumann@in.tum.de
• Wed, 04 Dec 2013
  • [isabelle] F-IDE 2014: Call for Papers - Peter Lammich, lammich@in.tum.de
  • [isabelle] A constant become a free variable - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] Isabelle2013-2-RC3 available for testing - bnord, bnord01@gmail.com
  • Re: [isabelle] Isabelle2013-2-RC3 available for testing - Makarius, makarius@sketis.net
  • Re: [isabelle] A constant become a free variable - Makarius, makarius@sketis.net
  • Re: [isabelle] Isabelle2013-2-RC3 available for testing - bnord, bnord01@gmail.com
  • Re: [isabelle] Isabelle2013-2-RC3 available for testing - Makarius, makarius@sketis.net
  • Re: [isabelle] Isabelle2013-2-RC3 available for testing - bnord, bnord01@gmail.com
  • [isabelle] Ctrl-Click on abbreviation from locale in image jumps to begin of context - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • Re: [isabelle] Ctrl-Click on abbreviation from locale in image jumps to begin of context - Makarius, makarius@sketis.net
  • Re: [isabelle] A constant become a free variable - Yannick, yannick_duchene@yahoo.fr
  • Re: [isabelle] A constant become a free variable - Makarius, makarius@sketis.net
  • Re: [isabelle] A constant become a free variable - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] A constant become a free variable - Makarius, makarius@sketis.net
  • Re: [isabelle] Ctrl-Click on abbreviation from locale in image jumps to begin of context - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • Re: [isabelle] Ctrl-Click on abbreviation from locale in image jumps to begin of context - Makarius, makarius@sketis.net
  • Re: [isabelle] Line numbers vs. icons - Gottfried Barrow, gottfried.barrow@gmx.com
  • [isabelle] Quotients, lifting and transfer in Isabelle2013-1 - Randy Pollack, rpollack@inf.ed.ac.uk
  • Re: [isabelle] Line numbers vs. icons - Makarius, makarius@sketis.net
  • Re: [isabelle] Isabelle2013-2-RC3 available for testing - Julian Brunner, julianbrunner@gmail.com
• Thu, 05 Dec 2013
  • [isabelle] Isabelle2013-2-RC3 ATP e_par acid test - Gottfried Barrow, gottfried.barrow@gmx.com
  • Re: [isabelle] Isabelle2013-2-RC3 ATP e_par acid test - Gottfried Barrow, gottfried.barrow@gmx.com
  • Re: [isabelle] Ctrl-Click on abbreviation from locale in image jumps to begin of context - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • Re: [isabelle] Ctrl-Click on abbreviation from locale in image jumps to begin of context - Makarius, makarius@sketis.net
  • Re: [isabelle] Ctrl-Click on abbreviation from locale in image jumps to begin of context - Makarius, makarius@sketis.net
  • Re: [isabelle] Ctrl-Click on abbreviation from locale in image jumps to begin of context - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • Re: [isabelle] Isabelle2013-2-RC3 ATP e_par acid test - Makarius, makarius@sketis.net
  • Re: [isabelle] Isabelle2013-2-RC3 ATP e_par acid test - Jasmin Christian Blanchette, jasmin.blanchette@gmail.com
  • Re: [isabelle] Isabelle2013-2-RC3 ATP e_par acid test - Gottfried Barrow, gottfried.barrow@gmx.com
  • [isabelle] ETH Zurich open PhD position in testing access control systems - Christoph Sprenger, sprenger@inf.ethz.ch
  • Re: [isabelle] Casting records efficiently - Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de
  • Re: [isabelle] exception using "case ... of ..." with HOLCF - Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de
  • Re: [isabelle] exception using "case ... of ..." with HOLCF - Dmitriy Traytel, traytel@in.tum.de
• Fri, 06 Dec 2013
  • [isabelle] ITP 2015 - Call for Bids - Gerwin Klein, Gerwin.Klein@nicta.com.au
  • [isabelle] Announcing Isabelle2013-2 - Makarius, makarius@sketis.net
  • Re: [isabelle] Announcing Isabelle2013-2 - Makarius, makarius@sketis.net
• Sun, 08 Dec 2013
  • [isabelle] Proof method to split disjunctions and conjunctions ? - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] Proof method to split disjunctions and conjunctions ? - Lawrence Paulson, lp15@cam.ac.uk
  • Re: [isabelle] Proof method to split disjunctions and conjunctions ? - Yannick, yannick_duchene@yahoo.fr
  • [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2. - David Greenaway, David.Greenaway@nicta.com.au
  • [isabelle] Data‑types: How to use discriminators? - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] Proof method to split disjunctions and conjunctions ? - Yannick, yannick_duchene@yahoo.fr
  • Re: [isabelle] Proof method to split disjunctions and conjunctions ? - Joachim Breitner, mail@joachim-breitner.de
  • Re: [isabelle] Proof method to split disjunctions and conjunctions ? - Lawrence Paulson, lp15@cam.ac.uk
  • [isabelle] Assertion failed - Joachim Breitner, breitner@kit.edu
  • Re: [isabelle] Quotients, lifting and transfer in Isabelle2013-1 - Gottfried Barrow, gottfried.barrow@gmx.com
  • Re: [isabelle] Data‑types: How to use discriminators? - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] Assertion failed - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] Data‑types: How to use discriminators? - Lawrence Paulson, lp15@cam.ac.uk
  • [isabelle] Cygwin script for SledgeH agsyHOL; leo2, yices, satallax local Cygwin installs - Gottfried Barrow, gottfried.barrow@gmx.com
• Mon, 09 Dec 2013
  • Re: [isabelle] Data‑types: How to use discriminators? - Yannick, yannick_duchene@yahoo.fr
  • [isabelle] Call for Industry Track Papers, FM 2014, May 2014, Singapore - Sun Jun, sunjun@sutd.edu.sg
  • Re: [isabelle] Data‑types: How to use discriminators? - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • Re: [isabelle] Data‑types: How to use discriminators? - Jasmin Blanchette, jasmin.blanchette@gmail.com
  • Re: [isabelle] Data‑types: How to use discriminators? - Yannick, yannick_duchene@yahoo.fr
  • Re: [isabelle] Data‑types: How to use discriminators? - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • Re: [isabelle] Data‑types: How to use discriminators? - Yannick, yannick_duchene@yahoo.fr
  • Re: [isabelle] Data‑types: How to use discriminators? - Yannick, yannick_duchene@yahoo.fr
  • Re: [isabelle] Data‑types: How to use discriminators? - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • [isabelle] jEdit print mode - Fabian Immler, immler@in.tum.de
  • Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2. - Lawrence Paulson, lp15@cam.ac.uk
  • Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2. - Makarius, makarius@sketis.net
  • [isabelle] Call for papers: Nonlinear Reasoning - Lawrence Paulson, lp15@cam.ac.uk
  • Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2. - David Greenaway, david.greenaway@nicta.com.au
  • Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2. - David Greenaway, david.greenaway@nicta.com.au
• Tue, 10 Dec 2013
  • Re: [isabelle] Quotients, lifting and transfer in Isabelle2013-1 - Ondřej Kunčar, kuncar@in.tum.de
  • Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2. - David Greenaway, david.greenaway@nicta.com.au
  • Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2. - Makarius, makarius@sketis.net
  • Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2. - Makarius, makarius@sketis.net
  • Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2. - Tobias Nipkow, nipkow@in.tum.de
  • Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2. - Makarius, makarius@sketis.net
  • Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2. - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2. - Makarius, makarius@sketis.net
  • Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2. - Lawrence Paulson, lp15@cam.ac.uk
  • Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2. - Lawrence Paulson, lp15@cam.ac.uk
  • Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2. - David Greenaway, david.greenaway@nicta.com.au
  • Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2. - David Greenaway, david.greenaway@nicta.com.au
• Wed, 11 Dec 2013
  • [isabelle] AFP 2013-2 released - Gerwin Klein, Gerwin.Klein@nicta.com.au
  • Re: [isabelle] AFP 2013-2 released - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2. - Lawrence Paulson, lp15@cam.ac.uk
  • Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2. - Makarius, makarius@sketis.net
  • Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2. - Makarius, makarius@sketis.net
  • Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2. - Lars Noschinski, noschinl@in.tum.de
  • Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2. - Gerwin Klein, Gerwin.Klein@nicta.com.au
• Thu, 12 Dec 2013
  • Re: [isabelle] Interpretation inside locale raises DUP - Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de
  • [isabelle] Parser in ML - li yongjian, lyj238@gmail.com
  • Re: [isabelle] Parser in ML - Lawrence Paulson, lp15@cam.ac.uk
• Fri, 13 Dec 2013
  • Re: [isabelle] Parser in ML - Michael Norrish, Michael.Norrish@nicta.com.au
  • Re: [isabelle] Parser in ML - Makarius, makarius@sketis.net
  • Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2. - Makarius, makarius@sketis.net
  • Re: [isabelle] lift_definition + constructor - Walther Neuper, wneuper@ist.tugraz.at
  • Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2. - Lawrence Paulson, lp15@cam.ac.uk
  • [isabelle] "(!!P. P::bool) ==> PROP P" with auto methods hangs PIDE - Gottfried Barrow, gottfried.barrow@gmx.com
  • Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2. - Makarius, makarius@sketis.net
• Sat, 14 Dec 2013
  • [isabelle] Infinitely recursive lambda expression or not? - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] Infinitely recursive lambda expression or not? - John Wickerson, johnwickerson@cantab.net
  • [isabelle] Hide all constructors of a datatype automatically - René Neumann, rene.neumann@in.tum.de
  • Re: [isabelle] Infinitely recursive lambda expression or not? - Yannick, yannick_duchene@yahoo.fr
  • Re: [isabelle] Infinitely recursive lambda expression or not? - Gottfried Barrow, gottfried.barrow@gmx.com
  • Re: [isabelle] Infinitely recursive lambda expression or not? - Lawrence Paulson, lp15@cam.ac.uk
  • Re: [isabelle] Hide all constructors of a datatype automatically - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] Hide all constructors of a datatype automatically - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] Infinitely recursive lambda expression or not? - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] Hide all constructors of a datatype automatically - Dmitriy Traytel, traytel@in.tum.de
  • Re: [isabelle] Infinitely recursive lambda expression or not? - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] Hide all constructors of a datatype automatically - René Neumann, rene.neumann@in.tum.de
  • Re: [isabelle] Infinitely recursive lambda expression or not? - Lawrence Paulson, lp15@cam.ac.uk
  • Re: [isabelle] Hide all constructors of a datatype automatically - Makarius, makarius@sketis.net
• Sun, 15 Dec 2013
  • [isabelle] (no subject) - li yongjian, lyj238@gmail.com
  • Re: [isabelle] (no subject) - Lawrence Paulson, lp15@cam.ac.uk
• Mon, 16 Dec 2013
  • Re: [isabelle] Announcing Isabelle2013-2 - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] lift_definition + constructor - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • Re: [isabelle] Announcing Isabelle2013-2 - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] Announcing Isabelle2013-2 - Peter Lammich, lammich@in.tum.de
  • Re: [isabelle] "(!!P. P::bool) ==> PROP P" with auto methods hangs PIDE - Makarius, makarius@sketis.net
  • Re: [isabelle] Interpretation inside locale raises DUP - Clemens Ballarin, ballarin@in.tum.de
• Tue, 17 Dec 2013
  • [isabelle] Missing transfer rules in quotient type - Daniel Raggi, danielraggi@gmail.com
  • Re: [isabelle] lift_definition + constructor - Walther Neuper, wneuper@ist.tugraz.at
  • Re: [isabelle] Missing transfer rules in quotient type - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • Re: [isabelle] Missing transfer rules in quotient type - Ondřej Kunčar, kuncar@in.tum.de
  • Re: [isabelle] Missing transfer rules in quotient type - Daniel Raggi, danielraggi@gmail.com
  • [isabelle] Proof failed in HOL? (build with -o browser_info fails) - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] Proof failed in HOL? (build with -o browser_info fails) - Peter Lammich, lammich@in.tum.de
• Wed, 18 Dec 2013
  • [isabelle] [Fwd: F-IDE 2014] - Peter Lammich, lammich@in.tum.de
  • [isabelle] isabelle build: number of threads - Christian Sternagel, c.sternagel@gmail.com
  • Re: [isabelle] "(!!P. P::bool) ==> PROP P" with auto methods hangs PIDE - Gottfried Barrow, gottfried.barrow@gmx.com
  • Re: [isabelle] Infinitely recursive lambda expression or not? - Gottfried Barrow, gottfried.barrow@gmx.com
  • [isabelle] Instantiating type classes - Manuel Eberl, eberlm@in.tum.de
• Thu, 19 Dec 2013
  • Re: [isabelle] Infinitely recursive lambda expression or not? - Gottfried Barrow, gottfried.barrow@gmx.com
  • [isabelle] [SOLVED] jedit mouse offset/menu bug with fullscreen window managers - David Cock, davec@cse.unsw.edu.au
  • Re: [isabelle] [SOLVED] jedit mouse offset/menu bug with fullscreen window managers - Christian Sternagel, c.sternagel@gmail.com
• Fri, 20 Dec 2013
  • [isabelle] Call for Papers: ITP 2014 - Gerwin Klein, Gerwin.Klein@nicta.com.au
  • [isabelle] where - Tobias Nipkow, nipkow@in.tum.de
  • Re: [isabelle] where - Jasmin Blanchette, jasmin.blanchette@gmail.com
• Sat, 21 Dec 2013
  • Re: [isabelle] Announcing Isabelle2013-2 - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] Announcing Isabelle2013-2 - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
• Sun, 22 Dec 2013
  • [isabelle] My unforgivable soundness issue with a locale - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] My unforgivable soundness issue with a locale - Peter Lammich, lammich@in.tum.de
• Mon, 23 Dec 2013
  • Re: [isabelle] My unforgivable soundness issue with a locale - Johannes Hölzl, hoelzl@in.tum.de
  • [isabelle] Does it mean busy or something else? (purple background) - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] My unforgivable soundness issue with a locale - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] My unforgivable soundness issue with a locale - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
• Tue, 24 Dec 2013
  • [isabelle] TYPES Meeting 2014 in Paris, 12 - 15 May: first call for contributions - Matthieu Sozeau, matthieu.sozeau@inria.fr
  • Re: [isabelle] My unforgivable soundness issue with a locale - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
• Wed, 25 Dec 2013
  • [isabelle] Are sorts of Isabelle the same as what's described for second order logic? - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] Are sorts of Isabelle the same as what's described for second order logic? - Lawrence Paulson, lp15@cam.ac.uk
  • Re: [isabelle] Are sorts of Isabelle the same as what's described for second order logic? - Christian Sternagel, c.sternagel@gmail.com
• Thu, 26 Dec 2013
  • Re: [isabelle] Where to learn about HOL vs FOL? - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] Are sorts of Isabelle the same as what's described for second order logic? - Yannick, yannick_duchene@yahoo.fr
  • Re: [isabelle] Infinitely recursive lambda expression or not? - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
• Fri, 27 Dec 2013
  • Re: [isabelle] Infinitely recursive lambda expression or not? - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] Infinitely recursive lambda expression or not? - Lawrence Paulson, lp15@cam.ac.uk
  • Re: [isabelle] Infinitely recursive lambda expression or not? - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] Infinitely recursive lambda expression or not? - Lawrence Paulson, lp15@cam.ac.uk
  • Re: [isabelle] Infinitely recursive lambda expression or not? - Yannick, yannick_duchene@yahoo.fr
• Sun, 29 Dec 2013
  • [isabelle] A problem on ML-like function programming - li yongjian, lyj238@gmail.com
  • Re: [isabelle] A problem on ML-like function programming - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] A problem on ML-like function programming - Lawrence Paulson, lp15@cam.ac.uk
  • Re: [isabelle] Where to learn about HOL vs FOL? - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] Where to learn about HOL vs FOL? - Lawrence Paulson, lp15@cam.ac.uk
  • [isabelle] Question on sequential pattern matching - Alessandro Coglio, coglio@kestrel.edu
• Mon, 30 Dec 2013
  • Re: [isabelle] Question on sequential pattern matching - Yannick Duchêne (Hibou57), yannick_duchene@yahoo.fr
  • Re: [isabelle] A problem on ML-like function programming - li yongjian, lyj238@gmail.com
  • Re: [isabelle] Question on sequential pattern matching - Alessandro Coglio, coglio@kestrel.edu
  • Re: [isabelle] Question on sequential pattern matching - Tobias Nipkow, nipkow@in.tum.de
  • [isabelle] Privacy by Design: from Theory to Practice (Postdoc Position at Inria in Lyon) - Daniel Le Métayer, daniel.le-metayer@inria.fr
• Tue, 31 Dec 2013
  • Re: [isabelle] Are sorts of Isabelle the same as what's described for second order logic? - Makarius, makarius@sketis.net