Cl-isabelle-users October 2013 Archives by date
- Tue, 01 Oct 2013
- Wed, 02 Oct 2013
- Thu, 03 Oct 2013
- 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
- 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
- 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
- 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
- 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
- Wed, 16 Oct 2013
- Thu, 17 Oct 2013
- Fri, 18 Oct 2013
- Sat, 19 Oct 2013
- Sun, 20 Oct 2013
- Mon, 21 Oct 2013
- Tue, 22 Oct 2013
- Wed, 23 Oct 2013
- 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
- Sun, 27 Oct 2013
- 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
- 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.