Cl-isabelle-users October 2013 Archives by date

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

• Tue, 01 Oct 2013
  • Re: [isabelle] undefined & None - Tobias Nipkow, nipkow@in.tum.de
  • Re: [isabelle] undefined & None - Tjark Weber, webertj@in.tum.de
  • Re: [isabelle] undefined & None - Peter Lammich, lammich@in.tum.de
  • Re: [isabelle] undefined & None - Tjark Weber, webertj@in.tum.de
• Wed, 02 Oct 2013
  • [isabelle] No type arity nat :: equal - Tobias Nipkow, nipkow@in.tum.de
  • [isabelle] CfP: AMAI Special Issue on Geometric Reasoning - Temur Kutsia, kutsia@risc.jku.at
  • Re: [isabelle] undefined & None - Makarius, makarius@sketis.net
  • Re: [isabelle] undefined & None - Makarius, makarius@sketis.net
  • Re: [isabelle] undefined & None - Joachim Breitner, breitner@kit.edu
• Thu, 03 Oct 2013
  • [isabelle] 2nd CfP (deadline 31 Oct) Math. in Comp. Sci. Special Issue 'Enabling Domain Experts to use Formalised Reasoning' - Christoph LANGE, math.semantic.web@gmail.com
  • [isabelle] Isabelle2013-1-RC1 available for testing - Makarius, makarius@sketis.net
  • [isabelle] Poor man's LaTeX markup for Isabelle listings - Christoph LANGE, math.semantic.web@gmail.com
  • [isabelle] 2013-1-RC1 'Find' GUI should wrap query string into "..." - Christoph LANGE, math.semantic.web@gmail.com
  • [isabelle] 2013-1-RC1: proof method suggested try or try0 no longer overwrites 'try' keyword - Christoph LANGE, math.semantic.web@gmail.com
  • [isabelle] value no longer pretty-prints numbers of type nat - Christoph LANGE, math.semantic.web@gmail.com
  • [isabelle] 2013-1-RC1: how to put generated Scala into a package without using code_include? - Christoph LANGE, math.semantic.web@gmail.com
  • Re: [isabelle] 2013-1-RC1: proof method suggested try or try0 no longer overwrites 'try' keyword - Christoph LANGE, math.semantic.web@gmail.com
• Fri, 04 Oct 2013
  • Re: [isabelle] 2013-1-RC1 'Find' GUI should wrap query string into "..." - Gerwin Klein, Gerwin.Klein@nicta.com.au
  • Re: [isabelle] 2013-1-RC1 'Find' GUI should wrap query string into "..." - Christoph LANGE, math.semantic.web@gmail.com
  • Re: [isabelle] Isabelle2013-1-RC1 available for testing - Christian Sternagel, c.sternagel@gmail.com
  • Re: [isabelle] 2013-1-RC1: how to put generated Scala into a package without using code_include? - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • [isabelle] type-unsound error - marco caminati, marco.caminati@yahoo.it
  • [isabelle] 2013-1-RC1: clicking on a README file in the documentation panel doesn't go to it if it's open already - Christoph LANGE, math.semantic.web@gmail.com
  • Re: [isabelle] type-unsound error - Jasmin Blanchette, jasmin.blanchette@gmail.com
  • Re: [isabelle] 2013-1-RC1: proof method suggested try or try0 no longer overwrites 'try' keyword - Makarius, makarius@sketis.net
  • Re: [isabelle] 2013-1-RC1: clicking on a README file in the documentation panel doesn't go to it if it's open already - Makarius, makarius@sketis.net
  • Re: [isabelle] 2013-1-RC1 'Find' GUI should wrap query string into "..." - Makarius, makarius@sketis.net
  • Re: [isabelle] type-unsound error - marco caminati, marco.caminati@yahoo.it
  • Re: [isabelle] Isabelle2013-1-RC1 available for testing - Makarius, makarius@sketis.net
  • Re: [isabelle] Isabelle2013-1-RC1 available for testing - Makarius, makarius@sketis.net
  • [isabelle] auto sledgehammer? [Re: 2013-1-RC1: proof method suggested try or try0 no longer overwrites 'try' keyword] - Christoph LANGE, math.semantic.web@gmail.com
  • Re: [isabelle] auto sledgehammer? [Re: 2013-1-RC1: proof method suggested try or try0 no longer overwrites 'try' keyword] - Makarius, makarius@sketis.net
• Sat, 05 Oct 2013
  • Re: [isabelle] 2013-1-RC1 'Find' GUI should wrap query string into "..." - Gerwin Klein, Gerwin.Klein@nicta.com.au
• Mon, 07 Oct 2013
  • Re: [isabelle] value no longer pretty-prints numbers of type nat - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • Re: [isabelle] auto sledgehammer? [Re: 2013-1-RC1: proof method suggested try or try0 no longer overwrites 'try' keyword] - Christoph LANGE, math.semantic.web@gmail.com
  • Re: [isabelle] auto sledgehammer? [Re: 2013-1-RC1: proof method suggested try or try0 no longer overwrites 'try' keyword] - Jasmin Blanchette, jasmin.blanchette@gmail.com
  • Re: [isabelle] 2013-1-RC1: how to put generated Scala into a package without using code_include? - C. Diekmann, diekmann@in.tum.de
  • Re: [isabelle] Poor man's LaTeX markup for Isabelle listings - Lawrence Paulson, lp15@cam.ac.uk
  • Re: [isabelle] Isabelle2013-1-RC1 available for testing - C. Diekmann, diekmann@in.tum.de
  • Re: [isabelle] 2013-1-RC1: how to put generated Scala into a package without using code_include? - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • Re: [isabelle] Isabelle2013-1-RC1 available for testing - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • Re: [isabelle] Isabelle2013-1-RC1 available for testing - Makarius, makarius@sketis.net
  • Re: [isabelle] Poor man's LaTeX markup for Isabelle listings - Tobias Nipkow, nipkow@in.tum.de
  • Re: [isabelle] Isabelle2013-1-RC1 available for testing - Makarius, makarius@sketis.net
  • [isabelle] Isabelle 2013 @ Fedora 64bits - Leo Freitas, leo.freitas@newcastle.ac.uk
  • Re: [isabelle] Isabelle 2013 @ Fedora 64bits - Makarius, makarius@sketis.net
  • Re: [isabelle] Poor man's LaTeX markup for Isabelle listings - Christoph LANGE, math.semantic.web@gmail.com
  • Re: [isabelle] Isabelle2013-1-RC1 available for testing - Makarius, makarius@sketis.net
  • Re: [isabelle] auto sledgehammer? [Re: 2013-1-RC1: proof method suggested try or try0 no longer overwrites 'try' keyword] - Christoph LANGE, math.semantic.web@gmail.com
  • Re: [isabelle] auto sledgehammer? [Re: 2013-1-RC1: proof method suggested try or try0 no longer overwrites 'try' keyword] - Christoph LANGE, math.semantic.web@gmail.com
  • [isabelle] Disable proof automation locally, per theorem? - Christoph LANGE, math.semantic.web@gmail.com
  • [isabelle] Auto sledgehammer fails to find proofs sledgehammer finds. - David Greenaway, david.greenaway@nicta.com.au
• Tue, 08 Oct 2013
  • Re: [isabelle] Isabelle2013-1-RC1 available for testing - Christian Sternagel, c.sternagel@gmail.com
  • Re: [isabelle] Poor man's LaTeX markup for Isabelle listings - Lawrence Paulson, lp15@cam.ac.uk
  • [isabelle] Fixed Points and Denotational Semantics - Alfio Martini, alfio.martini@acm.org
  • Re: [isabelle] Fixed Points and Denotational Semantics - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • [isabelle] Evaluation of record expressions - Michael Vu, michael.vu@rwth-aachen.de
  • Re: [isabelle] Isabelle2013-1-RC1 available for testing - C. Diekmann, diekmann@in.tum.de
  • Re: [isabelle] Fixed Points and Denotational Semantics - Brian Huffman, huffman.brian.c@gmail.com
  • Re: [isabelle] Fixed Points and Denotational Semantics - Alfio Martini, alfio.martini@acm.org
  • Re: [isabelle] Auto sledgehammer fails to find proofs sledgehammer finds. - Jasmin Blanchette, jasmin.blanchette@gmail.com
• Wed, 09 Oct 2013
  • Re: [isabelle] Isabelle2013-1-RC1 available for testing - C. Diekmann, diekmann@in.tum.de
  • Re: [isabelle] General code_abort'd constant - René Thiemann, rene.thiemann@uibk.ac.at
  • Re: [isabelle] Isabelle2013-1-RC1 available for testing - Makarius, makarius@sketis.net
  • Re: [isabelle] Fixed Points and Denotational Semantics - Viorel Preoteasaa, viorel.preoteasa@abo.fi
  • Re: [isabelle] Fixed Points and Denotational Semantics - Alfio Martini, alfio.martini@acm.org
  • [isabelle] Isabelle2013-1-RC2 available for testing - Makarius, makarius@sketis.net
  • Re: [isabelle] Isabelle2013-1-RC1 available for testing - Makarius, makarius@sketis.net
  • Re: [isabelle] General code_abort'd constant - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • [isabelle] Adding a code equation for a class parameter - Lars Hupel, hupel@in.tum.de
  • Re: [isabelle] Isabelle2013-1-RC2 available for testing - Christoph LANGE, math.semantic.web@gmail.com
  • Re: [isabelle] Adding a code equation for a class parameter - Lars Hupel, hupel@in.tum.de
  • Re: [isabelle] Adding a code equation for a class parameter - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • Re: [isabelle] Isabelle2013-1-RC2 available for testing - Makarius, makarius@sketis.net
  • Re: [isabelle] General code_abort'd constant - Makarius, makarius@sketis.net
  • Re: [isabelle] Isabelle2013-1-RC1 available for testing - Makarius, makarius@sketis.net
  • [isabelle] *.desktop entries and Arch packages [Re: Isabelle2013-1-RC2 available for testing] - Christoph LANGE, math.semantic.web@gmail.com
  • Re: [isabelle] Adding a code equation for a class parameter - Lars Hupel, hupel@in.tum.de
  • Re: [isabelle] *.desktop entries and Arch packages [Re: Isabelle2013-1-RC2 available for testing] - Makarius, makarius@sketis.net
  • Re: [isabelle] *.desktop entries and Arch packages [Re: Isabelle2013-1-RC2 available for testing] - Christoph LANGE, math.semantic.web@gmail.com
  • Re: [isabelle] *.desktop entries and Arch packages [Re: Isabelle2013-1-RC2 available for testing] - Makarius, makarius@sketis.net
  • Re: [isabelle] *.desktop entries and Arch packages [Re: Isabelle2013-1-RC2 available for testing] - Makarius, makarius@sketis.net
  • Re: [isabelle] *.desktop entries and Arch packages [Re: Isabelle2013-1-RC2 available for testing] - Christoph LANGE, math.semantic.web@gmail.com
  • Re: [isabelle] *.desktop entries and Arch packages [Re: Isabelle2013-1-RC2 available for testing] - Makarius, makarius@sketis.net
  • Re: [isabelle] *.desktop entries and Arch packages [Re: Isabelle2013-1-RC2 available for testing] - Christoph LANGE, math.semantic.web@gmail.com
  • Re: [isabelle] *.desktop entries and Arch packages [Re: Isabelle2013-1-RC2 available for testing] - Makarius, makarius@sketis.net
  • [isabelle] "Semantics of proofs and certified mathematics", IHP trimester, Paris, spring 2014: call for starting school application and workshop registration - Hugo Herbelin, Hugo.Herbelin@inria.fr
  • Re: [isabelle] Evaluation of record expressions - Andrew Boyton, Andrew.Boyton@nicta.com.au
  • Re: [isabelle] General code_abort'd constant - René Thiemann, rene.thiemann@uibk.ac.at
• Thu, 10 Oct 2013
  • [isabelle] No blast_trace anymore; assumption trace? - Gottfried Barrow, gottfried.barrow@gmx.com
  • Re: [isabelle] No blast_trace anymore; assumption trace? - Gottfried Barrow, gottfried.barrow@gmx.com
  • Re: [isabelle] RC2 for testing; Toplevel.timing has no affect anymore - Gottfried Barrow, gottfried.barrow@gmx.com
  • Re: [isabelle] RC2 for testing; Toplevel.timing has no affect anymore - Gottfried Barrow, gottfried.barrow@gmx.com
  • [isabelle] call for papers: Nonlinear Reasoning - Lawrence Paulson, lp15@cam.ac.uk
• Fri, 11 Oct 2013
  • [isabelle] RC2: jEdit macros don't work with \<^sub> in them - Gottfried Barrow, gottfried.barrow@gmx.com
  • Re: [isabelle] RC2: jEdit macros don't work with \<^sub> in them - Makarius, makarius@sketis.net
  • Re: [isabelle] RC2 for testing; Toplevel.timing has no affect anymore - Makarius, makarius@sketis.net
  • Re: [isabelle] RC2 for testing; Toplevel.timing has no affect anymore - Makarius, makarius@sketis.net
  • Re: [isabelle] No blast_trace anymore; assumption trace? - Makarius, makarius@sketis.net
  • Re: [isabelle] RC2 for testing; Toplevel.timing has no affect anymore - Makarius, makarius@sketis.net
  • Re: [isabelle] RC2 for testing; Toplevel.timing has no affect anymore - Gottfried Barrow, gottfried.barrow@gmx.com
  • Re: [isabelle] *.desktop entries and Arch packages [Re: Isabelle2013-1-RC2 available for testing] - René Neumann, rene.neumann@in.tum.de
  • Re: [isabelle] Evaluation of record expressions - Michael Vu, michael.vu@rwth-aachen.de
  • Re: [isabelle] RC2: jEdit macros don't work with \<^sub> in them - Gottfried Barrow, gottfried.barrow@gmx.com
  • Re: [isabelle] RC2: jEdit macros don't work with \<^sub> in them - Gottfried Barrow, gottfried.barrow@gmx.com
  • Re: [isabelle] RC2 for testing; Toplevel.timing has no affect anymore - Gottfried Barrow, gottfried.barrow@gmx.com
• Sat, 12 Oct 2013
  • Re: [isabelle] RC2: jEdit macros don't work with \<^sub> in them - Gottfried Barrow, gottfried.barrow@gmx.com
  • [isabelle] Isabelle 2013-1 RC2 (Documentation) - Alfio Martini, alfio.martini@acm.org
• Sun, 13 Oct 2013
  • Re: [isabelle] Isabelle 2013-1 RC2 (Documentation) - Tobias Nipkow, nipkow@in.tum.de
  • [isabelle] IMP Theories of the Book 'Concrete Semantics' - Alfio Martini, alfio.martini@acm.org
  • Re: [isabelle] IMP Theories of the Book 'Concrete Semantics' - Tobias Nipkow, nipkow@in.tum.de
  • Re: [isabelle] No type arity nat :: equal - Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de
  • Re: [isabelle] undefined & None - Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de
  • Re: [isabelle] undefined & None - Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de
  • Re: [isabelle] Adding a code equation for a class parameter - Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de
  • Re: [isabelle] value no longer pretty-prints numbers of type nat - Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de
  • Re: [isabelle] 2013-1-RC1: how to put generated Scala into a package without using code_include? - Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de
  • Re: [isabelle] 2013-1-RC1: how to put generated Scala into a package without using code_include? - Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de
• Mon, 14 Oct 2013
  • Re: [isabelle] Code generation from IArray - Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de
  • [isabelle] CfP: JSC Special Issue on Symbolic Computation in Software Science - Temur Kutsia, kutsia@risc.jku.at
  • Re: [isabelle] RC2: jEdit macros don't work with \<^sub> in them - Makarius, makarius@sketis.net
  • Re: [isabelle] RC2 for testing; Toplevel.timing has no affect anymore - Makarius, makarius@sketis.net
  • Re: [isabelle] Evaluation of record expressions - Michael Vu, michael.vu@rwth-aachen.de
  • Re: [isabelle] *.desktop entries and Arch packages [Re: Isabelle2013-1-RC2 available for testing] - Makarius, makarius@sketis.net
  • Re: [isabelle] Evaluation of record expressions - Jasmin Blanchette, jasmin.blanchette@gmail.com
  • Re: [isabelle] RC2 for testing; Toplevel.timing has no affect anymore - Makarius, makarius@sketis.net
  • Re: [isabelle] Evaluation of record expressions - Michael Vu, michael.vu@rwth-aachen.de
  • Re: [isabelle] RC2 for testing; Toplevel.timing has no affect anymore - Gottfried Barrow, gottfried.barrow@gmx.com
  • Re: [isabelle] Evaluation of record expressions - Jasmin Blanchette, jasmin.blanchette@gmail.com
  • Re: [isabelle] Evaluation of record expressions - Johannes Hölzl, hoelzl@in.tum.de
  • Re: [isabelle] RC2 for testing; Toplevel.timing has no affect anymore - Makarius, makarius@sketis.net
  • Re: [isabelle] RC2 for testing; Toplevel.timing has no affect anymore - Makarius, makarius@sketis.net
  • Re: [isabelle] Evaluation of record expressions - Michael Vu, michael.vu@rwth-aachen.de
  • Re: [isabelle] Evaluation of record expressions - Michael Vu, michael.vu@rwth-aachen.de
  • Re: [isabelle] RC2 for testing; Toplevel.timing has no affect anymore - Gottfried Barrow, gottfried.barrow@gmx.com
  • Re: [isabelle] RC2 for testing; Toplevel.timing has no affect anymore - Gottfried Barrow, gottfried.barrow@gmx.com
• Tue, 15 Oct 2013
  • Re: [isabelle] Isabelle2013-1-RC2 available for testing - Christian Sternagel, c.sternagel@gmail.com
  • Re: [isabelle] Evaluation of record expressions - Thomas Sewell, thomas.sewell@nicta.com.au
  • Re: [isabelle] RC2 for testing; Toplevel.timing has no affect anymore - Gottfried Barrow, gottfried.barrow@gmx.com
  • [isabelle] Problem "exception TYPE raised: Loose bound variable" - René Thiemann, rene.thiemann@uibk.ac.at
  • Re: [isabelle] RC2 for testing; Toplevel.timing has no affect anymore - Makarius, makarius@sketis.net
• Wed, 16 Oct 2013
  • [isabelle] Print Heading *before* theory (nice to have) - Holger Blasum, hbl@sysgo.com
  • Re: [isabelle] Print Heading *before* theory (nice to have) - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • Re: [isabelle] Print Heading *before* theory (nice to have) - Lars Noschinski, noschinl@in.tum.de
  • Re: [isabelle] Print Heading *before* theory (nice to have) - Holger Blasum, hbl@sysgo.com
  • Re: [isabelle] Print Heading *before* theory (nice to have) - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • Re: [isabelle] Print Heading *before* theory (nice to have) - Holger Blasum, hbl@sysgo.com
  • [isabelle] Isabelle2013-1-RC3 available for testing - Makarius, makarius@sketis.net
  • [isabelle] LaTeX specialised table env params vs Isabelle anti-quotations - Leo Freitas, leo.freitas@newcastle.ac.uk
  • Re: [isabelle] LaTeX specialised table env params vs Isabelle anti-quotations - Makarius, makarius@sketis.net
• Thu, 17 Oct 2013
  • [isabelle] Jedit: Spurious "Bad Theory" error - Peter Lammich, lammich@in.tum.de
  • Re: [isabelle] 2013-1-RC1: how to put generated Scala into a package without using code_include? - C. Diekmann, diekmann@in.tum.de
  • [isabelle] Jinja-Threads build problem - Peter Lammich, lammich@in.tum.de
• Fri, 18 Oct 2013
  • Re: [isabelle] Evaluation of record expressions - Michael Vu, michael.vu@rwth-aachen.de
  • Re: [isabelle] Evaluation of record expressions - Thomas Sewell, thomas.sewell@nicta.com.au
  • Re: [isabelle] Jinja-Threads build problem - Peter Lammich, lammich@in.tum.de
  • [isabelle] Recursion through Types - Tjark Weber, webertj@in.tum.de
  • [isabelle] Computing divisors - Manuel Eberl, eberlm@in.tum.de
  • Re: [isabelle] Computing divisors - Brian Huffman, huffman.brian.c@gmail.com
  • Re: [isabelle] Computing divisors - Manuel Eberl, eberlm@in.tum.de
• Sat, 19 Oct 2013
  • Re: [isabelle] Computing divisors - Ognjen Maric, ognjen.maric@gmail.com
  • Re: [isabelle] Computing divisors - René Thiemann, rene.thiemann@uibk.ac.at
  • Re: [isabelle] Computing divisors - Manuel Eberl, eberlm@in.tum.de
  • Re: [isabelle] Computing divisors - Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de
  • Re: [isabelle] Computing divisors - Manuel Eberl, eberlm@in.tum.de
  • Re: [isabelle] Computing divisors - Ognjen Maric, ognjen.maric@gmail.com
  • Re: [isabelle] Computing divisors - Manuel Eberl, eberlm@in.tum.de
• Sun, 20 Oct 2013
  • Re: [isabelle] Recursion through Types - Jesus Aransay, jesus-maria.aransay@unirioja.es
  • Re: [isabelle] IMP Theories of the Book 'Concrete Semantics' - Gergely Buday, gbuday@gmail.com
• Mon, 21 Oct 2013
  • Re: [isabelle] IMP Theories of the Book 'Concrete Semantics' - Tobias Nipkow, nipkow@in.tum.de
  • [isabelle] Session-Graph too large? - Peter Lammich, lammich@in.tum.de
  • Re: [isabelle] Recursion through Types - Johannes Hölzl, hoelzl@in.tum.de
  • [isabelle] Isabelle2013-1-RC3: setup_lifting raises TYPE - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • Re: [isabelle] Recursion through Types - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • [isabelle] Calling sublocale A < B in A’s context? - Joachim Breitner, breitner@kit.edu
  • Re: [isabelle] Calling sublocale A < B in A’s context? - Joachim Breitner, breitner@kit.edu
  • Re: [isabelle] Isabelle2013-1-RC3: setup_lifting raises TYPE - Ondřej Kunčar, kuncar@in.tum.de
• Tue, 22 Oct 2013
  • Re: [isabelle] 2013-1-RC1: how to put generated Scala into a package without using code_include? - Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de
  • Re: [isabelle] Computing divisors - Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de
• Wed, 23 Oct 2013
  • [isabelle] Problems using subclasses - René Thiemann, rene.thiemann@uibk.ac.at
  • Re: [isabelle] Problems using subclasses - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • [isabelle] Problem with Session-Creation - Burkhart Wolff, Burkhart.Wolff@lri.fr
  • Re: [isabelle] Problem with Session-Creation - Lars Noschinski, noschinl@in.tum.de
• Thu, 24 Oct 2013
  • [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping - Christian Sternagel, c.sternagel@gmail.com
  • Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping - Peter Lammich, lammich@in.tum.de
  • Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping - Christian Sternagel, c.sternagel@gmail.com
  • Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping - Ondřej Kunčar, kuncar@in.tum.de
  • [isabelle] Autocompletion in 2013-1 - Joachim Breitner, breitner@kit.edu
  • Re: [isabelle] Problems using subclasses - René Thiemann, rene.thiemann@uibk.ac.at
  • Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping - Christian Sternagel, c.sternagel@gmail.com
  • Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping - Ondřej Kunčar, kuncar@in.tum.de
• Fri, 25 Oct 2013
  • [isabelle] Call for participation: APLAS and CPP 2013 - Peter Schachte, schachte@unimelb.edu.au
  • Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping - Christian Sternagel, c.sternagel@gmail.com
  • Re: [isabelle] [isabelle-dev] Partial functions - Gottfried Barrow, gottfried.barrow@gmx.com
  • Re: [isabelle] [isabelle-dev] Partial functions - Christian Sternagel, c.sternagel@gmail.com
  • Re: [isabelle] 2013-1-RC1: how to put generated Scala into a package without using code_include? - C. Diekmann, diekmann@in.tum.de
  • Re: [isabelle] [isabelle-dev] Partial functions - Gottfried Barrow, gottfried.barrow@gmx.com
  • Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping - Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de
  • [isabelle] [Isabelle2013-1 RC] Scalability problem with re-entrant build of the whole distribution - Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de
  • Re: [isabelle] [Isabelle2013-1 RC] Scalability problem with re-entrant build of the whole distribution - Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de
• Sat, 26 Oct 2013
  • [isabelle] Relational & Algebraic Methods --- RAMiCS 2014 --- Final CFP, with Deadlines extended! - Wolfram Kahl, kahl@cas.mcmaster.ca
• Sun, 27 Oct 2013
  • [isabelle] Isabelle2013-1-RC3: try no longer seems to give preference to try0 over sledgehammer - Christoph LANGE, math.semantic.web@gmail.com
  • Re: [isabelle] Isabelle2013-1-RC3: try no longer seems to give preference to try0 over sledgehammer - Christoph LANGE, math.semantic.web@gmail.com
  • Re: [isabelle] [Isabelle2013-1 RC] Scalability problem with re-entrant build of the whole distribution - Stefan Berghofer, berghofe@in.tum.de
  • [isabelle] WRLA 2014 Call for papers - Santiago Escobar, sescobar@dsic.upv.es
• Mon, 28 Oct 2013
  • Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping - Dmitriy Traytel, traytel@in.tum.de
  • Re: [isabelle] Evaluation of record expressions - Michael Vu, michael.vu@rwth-aachen.de
• Tue, 29 Oct 2013
  • [isabelle] Lemmas about int_pow - Joachim Breitner, mail@joachim-breitner.de
  • [isabelle] Problems with elder Isabelle Versions under MacOSX Maverick - Burkhart Wolff, Burkhart.Wolff@lri.fr
  • Re: [isabelle] Problems with elder Isabelle Versions under MacOSX Maverick - Luca Ciciriello, luca_ciciriello@hotmail.com
  • Re: [isabelle] Lemmas about int_pow - Clemens Ballarin, ballarin@in.tum.de
• Wed, 30 Oct 2013
  • Re: [isabelle] Evaluation of record expressions - Thomas Sewell, thomas.sewell@nicta.com.au
  • [isabelle] (structure) and \<index> - bnord, bnord01@gmail.com
  • Re: [isabelle] (structure) and \<index> - Lars Noschinski, noschinl@in.tum.de
  • [isabelle] instantiation order for a record - Sven Schneider, Sven.Schneider@TU-Berlin.DE
  • Re: [isabelle] (structure) and \<index> - bnord, bnord01@gmail.com
  • Re: [isabelle] (structure) and \<index> - René Thiemann, rene.thiemann@uibk.ac.at
  • Re: [isabelle] instantiation order for a record - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • Re: [isabelle] instantiation order for a record - Sven Schneider, Sven.Schneider@TU-Berlin.DE
  • [isabelle] Product_Type.split_beta fails - Ognjen Maric, ognjen.maric@gmail.com
  • [isabelle] Trouble loading theories on windows (Isabelle2013-1-RC3) - Gottfried Barrow, gottfried.barrow@gmx.com
• Thu, 31 Oct 2013
  • Re: [isabelle] Trouble loading theories on windows (Isabelle2013-1-RC3) - Gottfried Barrow, gottfried.barrow@gmx.com
  • [isabelle] PhD and PostDoc Positions at the University of Innsbruck, Austria - Cezary Kaliszyk, cezarykaliszyk@gmail.com
  • [isabelle] PDFs for HOL-BNF? Tutorials for transfer, lifting, and quotients? - Gottfried Barrow, gottfried.barrow@gmx.com
  • [isabelle] "code_pred" introduces axioms? - Jasmin Christian Blanchette, jasmin.blanchette@gmail.com
  • Re: [isabelle] "code_pred" introduces axioms? - Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch
  • Re: [isabelle] "code_pred" introduces axioms? - Jasmin Blanchette, jasmin.blanchette@gmail.com
  • Re: [isabelle] (structure) and \<index> - Clemens Ballarin, ballarin@in.tum.de
  • Re: [isabelle] (structure) and \<index> - bnord, bnord01@gmail.com