Cl-isabelle-users January 2016 Archives by subject
- Re: [isabelle] Funny font metrics in the Search and Replace dialog [Isabelle2016-RC2]
- Re: [isabelle] "apply auto" transforms provable statement to something false?
- [isabelle] "apply auto" transforms provable statement to something false?
- Eugene W. Stark, isabelle-users@starkeffect.com - Mon, 25 Jan 2016 11:02:39 +0000
- [isabelle] "defines" in a locale
- Peter Gammie, peteg42@gmail.com - Mon, 25 Jan 2016 04:41:14 +0000
- Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch - Mon, 25 Jan 2016 09:53:31 +0000
- Peter Gammie, peteg42@gmail.com - Tue, 26 Jan 2016 03:38:06 +0000
- [isabelle] 4 new AFP entries
- Gerwin Klein, Gerwin.Klein@nicta.com.au - Tue, 05 Jan 2016 23:12:35 +0000
- [isabelle] Funny font metrics in the Search and Replace dialog [Isabelle2016-RC2]
- Re: [isabelle] A proof on moreover and ultimately
- Makarius, makarius@sketis.net - Fri, 01 Jan 2016 20:18:40 +0000
- [isabelle] axiom of choice in Isabelle/HOL, and sledgehammer
- dimitri, dimitri@math.uni-bonn.de - Tue, 26 Jan 2016 20:16:39 +0000
- [isabelle] Blog: Release candidates for Isabelle2016
- Makarius, makarius@sketis.net - Fri, 15 Jan 2016 20:48:48 +0000
- [isabelle] building session confuses paths to theories
- Walther Neuper, wneuper@ist.tugraz.at - Tue, 12 Jan 2016 11:35:34 +0000
- Peter Lammich, lammich@in.tum.de - Tue, 12 Jan 2016 12:23:24 +0000
- Walther Neuper, wneuper@ist.tugraz.at - Wed, 13 Jan 2016 14:04:44 +0000
- Makarius, makarius@sketis.net - Wed, 13 Jan 2016 20:10:01 +0000
- [isabelle] Cantor's Theorem
- Makarius, makarius@sketis.net - Fri, 01 Jan 2016 21:34:00 +0000
- [isabelle] Changes to ML File structure in Isabelle2016-RC0
- Eugene W. Stark, isabelle-users@starkeffect.com - Thu, 14 Jan 2016 23:57:32 +0000
- Makarius, makarius@sketis.net - Fri, 15 Jan 2016 10:57:54 +0000
- [isabelle] Code equations for "power"
- Manuel Eberl, eberlm@in.tum.de - Fri, 08 Jan 2016 15:03:56 +0000
- Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch - Fri, 08 Jan 2016 16:17:28 +0000
- Manuel Eberl, eberlm@in.tum.de - Fri, 08 Jan 2016 16:28:41 +0000
- Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch - Fri, 08 Jan 2016 16:39:06 +0000
- Thiemann, Rene, Rene.Thiemann@uibk.ac.at - Mon, 11 Jan 2016 08:23:37 +0000
- [isabelle] COLAFORM @ ENASE 2016: Deadline extended
- Maria Spichkova, maria.spichkova@rmit.edu.au - Tue, 19 Jan 2016 04:50:46 +0000
- [isabelle] Common sub-expression elimination
- Manuel Eberl, eberlm@in.tum.de - Tue, 19 Jan 2016 10:31:26 +0000
- Ramana Kumar, rk436@cam.ac.uk - Tue, 19 Jan 2016 10:49:07 +0000
- Manuel Eberl, eberlm@in.tum.de - Tue, 19 Jan 2016 11:18:44 +0000
- Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch - Mon, 25 Jan 2016 08:38:49 +0000
- [isabelle] Deep embedding of natural deduction?
- [isabelle] Dockable panels
- Lawrence Paulson, lp15@cam.ac.uk - Mon, 18 Jan 2016 16:53:42 +0000
- Makarius, makarius@sketis.net - Mon, 18 Jan 2016 19:22:23 +0000
- Lawrence Paulson, lp15@cam.ac.uk - Tue, 19 Jan 2016 10:42:47 +0000
- Makarius, makarius@sketis.net - Tue, 19 Jan 2016 10:48:01 +0000
- Lawrence Paulson, lp15@cam.ac.uk - Tue, 19 Jan 2016 10:56:15 +0000
- Jasmin Blanchette, jasmin.blanchette@inria.fr - Tue, 19 Jan 2016 11:15:28 +0000
- Lars Hupel, hupel@in.tum.de - Tue, 19 Jan 2016 11:24:22 +0000
- bnord, bnord01@gmail.com - Tue, 19 Jan 2016 11:24:44 +0000
- Tobias Nipkow, nipkow@in.tum.de - Tue, 19 Jan 2016 12:02:23 +0000
- Makarius, makarius@sketis.net - Tue, 19 Jan 2016 12:48:15 +0000
- bnord, bnord01@gmail.com - Tue, 19 Jan 2016 13:42:41 +0000
- Makarius, makarius@sketis.net - Tue, 19 Jan 2016 14:08:18 +0000
- Jasmin Blanchette, jasmin.blanchette@inria.fr - Tue, 19 Jan 2016 15:03:05 +0000
- Makarius, makarius@sketis.net - Tue, 19 Jan 2016 15:11:30 +0000
- Lawrence Paulson, lp15@cam.ac.uk - Tue, 19 Jan 2016 15:21:17 +0000
- Makarius, makarius@sketis.net - Tue, 19 Jan 2016 15:42:37 +0000
- Lawrence Paulson, lp15@cam.ac.uk - Tue, 19 Jan 2016 15:46:10 +0000
- bnord, bnord01@gmail.com - Tue, 19 Jan 2016 15:50:42 +0000
- Jasmin Blanchette, jasmin.blanchette@inria.fr - Tue, 19 Jan 2016 15:56:37 +0000
- bnord, bnord01@gmail.com - Tue, 19 Jan 2016 16:05:52 +0000
- Simon Wimmer, wimmersimon@gmail.com - Tue, 19 Jan 2016 16:33:37 +0000
- bnord, bnord01@gmail.com - Tue, 19 Jan 2016 17:32:41 +0000
- Makarius, makarius@sketis.net - Tue, 19 Jan 2016 17:50:50 +0000
- bnord, bnord01@gmail.com - Tue, 19 Jan 2016 20:29:47 +0000
- Eugene W. Stark, isabelle-users@starkeffect.com - Tue, 19 Jan 2016 22:50:30 +0000
- Makarius, makarius@sketis.net - Wed, 20 Jan 2016 12:42:25 +0000
- [isabelle] Dysfunctional complete lattice syntax [was: Isabelle2016-RC0 available for testing]
- Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de - Sun, 03 Jan 2016 15:47:33 +0000
- Makarius, makarius@sketis.net - Sun, 03 Jan 2016 21:15:36 +0000
- Florian Haftmann, florian.haftmann@informatik.tu-muenchen.de - Mon, 04 Jan 2016 18:43:33 +0000
- Re: [isabelle] Eisbach: Method command: Documentation text
- Makarius, makarius@sketis.net - Sat, 09 Jan 2016 19:55:21 +0000
- Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?
- Ramana Kumar, rk436@cam.ac.uk - Tue, 12 Jan 2016 02:43:26 +0000
- Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch - Tue, 12 Jan 2016 07:20:52 +0000
- Thiemann, Rene, Rene.Thiemann@uibk.ac.at - Tue, 12 Jan 2016 08:05:16 +0000
- Eugene W. Stark, isabelle-users@starkeffect.com - Tue, 12 Jan 2016 10:05:36 +0000
- Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch - Tue, 12 Jan 2016 11:13:48 +0000
- Eugene W. Stark, isabelle-users@starkeffect.com - Tue, 12 Jan 2016 11:26:52 +0000
- [isabelle] Failure to prove a simple transitivity -- what could be the cause?
- Eugene W. Stark, isabelle-users@starkeffect.com - Mon, 11 Jan 2016 20:47:44 +0000
- [isabelle] Final CFP: Diagrams 2016 (9th Int'l Conference on the Theory and Application of Diagrams)
- [isabelle] Folding by indentation broken in 2016-RC1 [was: Isabelle2016-RC1 available for testing]
- bnord, bnord01@gmail.com - Wed, 20 Jan 2016 11:03:36 +0000
- Makarius, makarius@sketis.net - Sun, 24 Jan 2016 19:57:49 +0000
- bnord, bnord01@gmail.com - Mon, 25 Jan 2016 10:39:27 +0000
- bnord, bnord01@gmail.com - Mon, 25 Jan 2016 10:52:00 +0000
- Re: [isabelle] function internals in Isabelle2016-RC1
- Thiemann, Rene, Rene.Thiemann@uibk.ac.at - Mon, 18 Jan 2016 11:16:40 +0000
- Makarius, makarius@sketis.net - Tue, 19 Jan 2016 10:50:11 +0000
- Thiemann, Rene, Rene.Thiemann@uibk.ac.at - Tue, 19 Jan 2016 11:54:38 +0000
- [isabelle] Funded Doctoral Positions in Computer Science in Austria (LogiCS)
- list-announcer, list-announcer@dbai.tuwien.ac.at - Fri, 29 Jan 2016 10:34:55 +0000
- Re: [isabelle] Funny font metrics in the Search and Replace dialog [Isabelle2016-RC2]
- Makarius, makarius@sketis.net - Tue, 26 Jan 2016 23:12:56 +0000
- Makarius, makarius@sketis.net - Thu, 28 Jan 2016 16:19:19 +0000
- Makarius, makarius@sketis.net - Fri, 29 Jan 2016 12:40:52 +0000
- Makarius, makarius@sketis.net - Fri, 29 Jan 2016 19:23:49 +0000
- Re: [isabelle] Goal.prove automatically produces schematic type variables
- Makarius, makarius@sketis.net - Tue, 12 Jan 2016 23:00:33 +0000
- [isabelle] Goal.prove automatically produces schematic type variables
- Bohua Zhan, bzhan@mit.edu - Tue, 12 Jan 2016 20:28:36 +0000
- [isabelle] Goedel's paradox, canonical definitions vs. instances/models (dependent type theory and the language of species), expressiveness vs. automation, re-evaluating natural deduction
- Ken Kubota, mail@kenkubota.de - Tue, 26 Jan 2016 15:04:09 +0000
- [isabelle] HCVS 2016: 3rd Workshop on Horn Clauses for Verification and Synthesis
- Philipp Ruemmer, philipp.ruemmer@it.uu.se - Mon, 18 Jan 2016 13:55:54 +0000
- [isabelle] Induction principle for datatypes
- çæç, wangsl@ios.ac.cn - Fri, 29 Jan 2016 04:15:22 +0000
- Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch - Fri, 29 Jan 2016 06:34:58 +0000
- çæç, wangsl@ios.ac.cn - Fri, 29 Jan 2016 10:13:30 +0000
- [isabelle] Isabelle 2016 RC1: multiset changes
- Bertram Felgenhauer via Cl-isabelle-users, cl-isabelle-users@lists.cam.ac.uk - Wed, 20 Jan 2016 14:52:52 +0000
- Fleury Mathias, mathias.fleury12@gmail.com - Wed, 20 Jan 2016 15:30:45 +0000
- Fleury Mathias, mathias.fleury12@gmail.com - Wed, 20 Jan 2016 16:04:15 +0000
- Bertram Felgenhauer via Cl-isabelle-users, cl-isabelle-users@lists.cam.ac.uk - Wed, 20 Jan 2016 16:43:00 +0000
- Jasmin Blanchette, jasmin.blanchette@inria.fr - Wed, 20 Jan 2016 17:17:52 +0000
- Bertram Felgenhauer via Cl-isabelle-users, cl-isabelle-users@lists.cam.ac.uk - Thu, 21 Jan 2016 13:32:15 +0000
- [isabelle] Isabelle 2016-RC2: warnings in generated code for GCD and LCM
- Thiemann, Rene, Rene.Thiemann@uibk.ac.at - Thu, 28 Jan 2016 15:26:16 +0000
- [isabelle] Isabelle-RCX/Windows 64 bits (Sledgehammer)
- Alfio Martini, alfio.martini@acm.org - Fri, 29 Jan 2016 16:04:07 +0000
- Re: [isabelle] Isabelle2016-RC0 - A fast implementation of concat for strings?
- C. Diekmann, diekmann@in.tum.de - Sun, 03 Jan 2016 21:02:20 +0000
- Re: [isabelle] Isabelle2016-RC0 - AFP and Library available for testing
- C. Diekmann, diekmann@in.tum.de - Sat, 02 Jan 2016 13:23:02 +0000
- Makarius, makarius@sketis.net - Sat, 02 Jan 2016 15:53:46 +0000
- Makarius, makarius@sketis.net - Sun, 03 Jan 2016 21:33:00 +0000
- Gerwin Klein, Gerwin.Klein@nicta.com.au - Mon, 04 Jan 2016 22:12:35 +0000
- Gerwin Klein, Gerwin.Klein@nicta.com.au - Mon, 11 Jan 2016 01:17:38 +0000
- Makarius, makarius@sketis.net - Sat, 16 Jan 2016 13:20:28 +0000
- Daniel Matichuk, Daniel.Matichuk@nicta.com.au - Mon, 18 Jan 2016 05:46:23 +0000
- Re: [isabelle] Isabelle2016-RC0 - default output buffers
- C. Diekmann, diekmann@in.tum.de - Sun, 03 Jan 2016 16:38:52 +0000
- Makarius, makarius@sketis.net - Sun, 03 Jan 2016 21:51:19 +0000
- C. Diekmann, diekmann@in.tum.de - Mon, 04 Jan 2016 18:20:55 +0000
- Julian Brunner, julianbrunner@gmail.com - Thu, 07 Jan 2016 18:06:35 +0000
- Tobias Nipkow, nipkow@in.tum.de - Thu, 07 Jan 2016 18:18:52 +0000
- Makarius, makarius@sketis.net - Fri, 08 Jan 2016 15:33:48 +0000
- Makarius, makarius@sketis.net - Fri, 08 Jan 2016 15:36:43 +0000
- Tobias Nipkow, nipkow@in.tum.de - Sat, 09 Jan 2016 11:23:18 +0000
- Makarius, makarius@sketis.net - Sat, 09 Jan 2016 12:21:39 +0000
- Tobias Nipkow, nipkow@in.tum.de - Mon, 11 Jan 2016 17:03:31 +0000
- Lawrence Paulson, lp15@cam.ac.uk - Mon, 11 Jan 2016 17:11:35 +0000
- Makarius, makarius@sketis.net - Mon, 11 Jan 2016 20:07:58 +0000
- Re: [isabelle] Isabelle2016-RC0 - does not exit on Linux
- C. Diekmann, diekmann@in.tum.de - Sun, 03 Jan 2016 21:18:59 +0000
- Makarius, makarius@sketis.net - Mon, 04 Jan 2016 21:43:37 +0000
- Lars Hupel, hupel@in.tum.de - Mon, 04 Jan 2016 21:49:49 +0000
- Makarius, makarius@sketis.net - Mon, 04 Jan 2016 22:48:27 +0000
- Makarius, makarius@sketis.net - Tue, 05 Jan 2016 13:30:18 +0000
- Re: [isabelle] Isabelle2016-RC0 - isar-ref.pdf datatype documentation
- C. Diekmann, diekmann@in.tum.de - Sun, 03 Jan 2016 17:12:47 +0000
- Re: [isabelle] Isabelle2016-RC0 - output says "theorem" when I called it a "lemma"
- Makarius, makarius@sketis.net - Fri, 15 Jan 2016 21:55:52 +0000
- [isabelle] Isabelle2016-RC0 - output says "theorem" when I called it a "lemma"
- Eugene W. Stark, isabelle-users@starkeffect.com - Fri, 15 Jan 2016 21:29:14 +0000
- Re: [isabelle] Isabelle2016-RC0 - overloaded datatypes
- C. Diekmann, diekmann@in.tum.de - Sun, 03 Jan 2016 16:54:33 +0000
- Makarius, makarius@sketis.net - Tue, 19 Jan 2016 23:05:12 +0000
- Re: [isabelle] Isabelle2016-RC0 - using goal_cases correctly
- C. Diekmann, diekmann@in.tum.de - Sun, 03 Jan 2016 18:12:44 +0000
- Makarius, makarius@sketis.net - Sat, 09 Jan 2016 18:59:12 +0000
- Re: [isabelle] Isabelle2016-RC0 - zpower_int disappeared
- [isabelle] Isabelle2016-RC0 available for testing
- Makarius, makarius@sketis.net - Fri, 01 Jan 2016 19:18:01 +0000
- Lars Hupel, hupel@in.tum.de - Fri, 01 Jan 2016 20:30:15 +0000
- Makarius, makarius@sketis.net - Fri, 01 Jan 2016 20:42:12 +0000
- Lars Hupel, hupel@in.tum.de - Fri, 01 Jan 2016 21:15:35 +0000
- Makarius, makarius@sketis.net - Fri, 01 Jan 2016 21:25:26 +0000
- Lars Hupel, hupel@in.tum.de - Fri, 01 Jan 2016 22:01:32 +0000
- [isabelle] Isabelle2016-RC0: cvc4 crashing
- Eugene W. Stark, isabelle-users@starkeffect.com - Thu, 14 Jan 2016 16:53:25 +0000
- Jasmin Blanchette, jasmin.blanchette@inria.fr - Thu, 14 Jan 2016 18:46:08 +0000
- Eugene W. Stark, isabelle-users@starkeffect.com - Thu, 14 Jan 2016 18:49:47 +0000
- Jasmin Blanchette, jasmin.blanchette@inria.fr - Thu, 14 Jan 2016 19:36:23 +0000
- Eugene W. Stark, isabelle-users@starkeffect.com - Thu, 14 Jan 2016 19:43:44 +0000
- Jasmin Blanchette, jasmin.blanchette@inria.fr - Thu, 14 Jan 2016 20:24:03 +0000
- Makarius, makarius@sketis.net - Sun, 31 Jan 2016 20:52:02 +0000
- Eugene W. Stark, isabelle-users@starkeffect.com - Sun, 31 Jan 2016 21:59:15 +0000
- [isabelle] Isabelle2016-RC0: font size of diamond symbol
- Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch - Fri, 08 Jan 2016 08:24:39 +0000
- Makarius, makarius@sketis.net - Sat, 09 Jan 2016 19:06:59 +0000
- [isabelle] Isabelle2016-RC0: HiDPI + Linux
- Corey Richardson, corey@octayn.net - Tue, 12 Jan 2016 16:24:48 +0000
- Makarius, makarius@sketis.net - Wed, 13 Jan 2016 14:11:32 +0000
- Makarius, makarius@sketis.net - Wed, 13 Jan 2016 14:16:34 +0000
- Makarius, makarius@sketis.net - Wed, 13 Jan 2016 14:36:24 +0000
- Corey Richardson, corey@octayn.net - Wed, 13 Jan 2016 15:22:18 +0000
- Corey Richardson, corey@octayn.net - Wed, 13 Jan 2016 15:27:15 +0000
- Makarius, makarius@sketis.net - Wed, 13 Jan 2016 15:35:50 +0000
- Re: [isabelle] Isabelle2016-RC0: symbols sometimes displayed as ASCII strings
- Makarius, makarius@sketis.net - Fri, 08 Jan 2016 17:29:07 +0000
- [isabelle] Isabelle2016-RC0: symbols sometimes displayed as ASCII strings
- Giuliano Losa, giuliano@losa.fr - Thu, 07 Jan 2016 21:41:13 +0000
- [isabelle] Isabelle2016-RC0: Windows bootstrapping
- Lars Hupel, hupel@in.tum.de - Wed, 06 Jan 2016 21:59:37 +0000
- Lars Hupel, hupel@in.tum.de - Wed, 06 Jan 2016 22:26:10 +0000
- Makarius, makarius@sketis.net - Wed, 06 Jan 2016 23:18:52 +0000
- Lars Hupel, hupel@in.tum.de - Thu, 07 Jan 2016 08:56:32 +0000
- Makarius, makarius@sketis.net - Thu, 07 Jan 2016 12:17:43 +0000
- Lars Hupel, hupel@in.tum.de - Thu, 07 Jan 2016 12:33:29 +0000
- Lars Hupel, hupel@in.tum.de - Thu, 07 Jan 2016 12:47:32 +0000
- Makarius, makarius@sketis.net - Fri, 08 Jan 2016 16:21:34 +0000
- [isabelle] Isabelle2016-RC1 -- untidy stack trace output generated
- Eugene W. Stark, isabelle-users@starkeffect.com - Fri, 15 Jan 2016 21:47:20 +0000
- Makarius, makarius@sketis.net - Fri, 15 Jan 2016 22:06:29 +0000
- [isabelle] Isabelle2016-RC1 available for testing
- Makarius, makarius@sketis.net - Fri, 15 Jan 2016 20:27:44 +0000
- Re: [isabelle] Isabelle2016-RC1 blue screen of death
- Makarius, makarius@sketis.net - Fri, 22 Jan 2016 19:20:06 +0000
- [isabelle] Isabelle2016-RC1: typedef-overloaded and records
- Thiemann, Rene, Rene.Thiemann@uibk.ac.at - Mon, 18 Jan 2016 11:51:12 +0000
- Dmitriy Traytel, traytel@inf.ethz.ch - Mon, 18 Jan 2016 17:10:01 +0000
- C. Diekmann, diekmann@in.tum.de - Tue, 19 Jan 2016 22:16:58 +0000
- Re: [isabelle] Isabelle2016-RC2 available (Editor's Text Area vs File)
- Alfio Martini, alfio.martini@acm.org - Thu, 28 Jan 2016 14:58:06 +0000
- Makarius, makarius@sketis.net - Thu, 28 Jan 2016 15:21:35 +0000
- Alfio Martini, alfio.martini@acm.org - Thu, 28 Jan 2016 15:42:52 +0000
- Makarius, makarius@sketis.net - Thu, 28 Jan 2016 16:06:08 +0000
- Alfio Martini, alfio.martini@acm.org - Thu, 28 Jan 2016 16:16:22 +0000
- [isabelle] Isabelle2016-RC2 available for testing
- Makarius, makarius@sketis.net - Sun, 24 Jan 2016 21:17:36 +0000
- Re: [isabelle] Isabelle2016-RC2 Java exceptions related to search/replace
- Makarius, makarius@sketis.net - Sun, 31 Jan 2016 20:44:56 +0000
- Eugene W. Stark, isabelle-users@starkeffect.com - Sun, 31 Jan 2016 22:05:51 +0000
- Makarius, makarius@sketis.net - Sun, 31 Jan 2016 22:27:20 +0000
- [isabelle] Isabelle2016-RC2 Java exceptions related to search/replace
- Eugene W. Stark, isabelle-users@starkeffect.com - Fri, 29 Jan 2016 13:14:39 +0000
- [isabelle] Isabelle2016-RC2 JEdit lockup with Java at 100% CPU
- Eugene W. Stark, isabelle-users@starkeffect.com - Fri, 29 Jan 2016 23:30:44 +0000
- Makarius, makarius@sketis.net - Sun, 31 Jan 2016 20:06:31 +0000
- Re: [isabelle] Isabelle2016-RC2 JEdit lockup with Java at 100% CPU (was: Re: Isabelle2016-RC2 Java exceptions related to search/replace)
- Eugene W. Stark, isabelle-users@starkeffect.com - Sun, 31 Jan 2016 22:34:19 +0000
- Makarius, makarius@sketis.net - Sun, 31 Jan 2016 22:46:58 +0000
- [isabelle] Isabelle2016-RC2 panel focus issues
- Eugene W. Stark, isabelle-users@starkeffect.com - Fri, 29 Jan 2016 13:46:25 +0000
- Makarius, makarius@sketis.net - Fri, 29 Jan 2016 14:57:39 +0000
- Eugene W. Stark, isabelle-users@starkeffect.com - Fri, 29 Jan 2016 15:01:11 +0000
- Makarius, makarius@sketis.net - Fri, 29 Jan 2016 23:11:52 +0000
- Eugene W. Stark, isabelle-users@starkeffect.com - Fri, 29 Jan 2016 23:39:22 +0000
- [isabelle] Isabelle2016-RC2: bogus simplifier trace messages
- Lars Hupel, hupel@in.tum.de - Thu, 28 Jan 2016 14:14:37 +0000
- Makarius, makarius@sketis.net - Fri, 29 Jan 2016 16:07:21 +0000
- Re: [isabelle] Isabelle2016-RC2: jdk-8u72
- Makarius, makarius@sketis.net - Sun, 24 Jan 2016 21:30:45 +0000
- Re: [isabelle] Juxtaposed cartouche error in session run; okay in PIDE
- [isabelle] lift_bnf Subscript exception
- [isabelle] New AFP article: Knot Theory
- Tobias Nipkow, nipkow@in.tum.de - Wed, 20 Jan 2016 11:34:30 +0000
- [isabelle] New AFP entry: Tensor Product of Matrices
- Tobias Nipkow, nipkow@in.tum.de - Mon, 18 Jan 2016 18:04:38 +0000
- [isabelle] new in the AFP: Cardinality of Number Partitions
- [isabelle] Postdoc position on hardware verification at NTU Singapore
- Alwen Tiu, alwen.tiu@gmail.com - Wed, 20 Jan 2016 02:07:39 +0000
- Re: [isabelle] Postdoc position on security protocol verification at NTU Singapore
- Alwen Tiu, alwen.tiu@gmail.com - Wed, 20 Jan 2016 01:54:23 +0000
- [isabelle] Postdoc position on security protocol verification at NTU Singapore
- Alwen Tiu, alwen.tiu@gmail.com - Wed, 20 Jan 2016 01:46:06 +0000
- [isabelle] Problem with induction_schema
- Manuel Eberl, eberlm@in.tum.de - Fri, 29 Jan 2016 13:43:10 +0000
- [isabelle] program verification using denotational semantics
- Buday Gergely, gbuday@karolyrobert.hu - Wed, 13 Jan 2016 14:41:53 +0000
- Re: [isabelle] Program verification using denotational semantics
- [isabelle] RC1 - Greyout
- Peter Lammich, lammich@in.tum.de - Thu, 21 Jan 2016 12:58:32 +0000
- Peter Lammich, lammich@in.tum.de - Thu, 21 Jan 2016 15:06:54 +0000
- Makarius, makarius@sketis.net - Thu, 21 Jan 2016 15:48:07 +0000
- Lars Hupel, hupel@in.tum.de - Wed, 27 Jan 2016 10:06:43 +0000
- Simon Wimmer, wimmersimon@gmail.com - Wed, 27 Jan 2016 10:18:05 +0000
- Makarius, makarius@sketis.net - Wed, 27 Jan 2016 14:30:09 +0000
- Lars Hupel, hupel@in.tum.de - Thu, 28 Jan 2016 18:42:13 +0000
- [isabelle] RC1: Basic_BNFs.snds
- Re: [isabelle] RC1: etc/symbols file from 2015 crashes jedit tool on startup
- Lars Hupel, hupel@in.tum.de - Thu, 21 Jan 2016 13:37:43 +0000
- Peter Lammich, lammich@in.tum.de - Thu, 21 Jan 2016 14:08:47 +0000
- Lars Hupel, hupel@in.tum.de - Thu, 21 Jan 2016 14:23:33 +0000
- bnord, bnord01@gmail.com - Thu, 21 Jan 2016 14:33:22 +0000
- Peter Lammich, lammich@in.tum.de - Thu, 21 Jan 2016 14:58:11 +0000
- Makarius, makarius@sketis.net - Thu, 21 Jan 2016 20:50:05 +0000
- [isabelle] RC1: etc/symbols file from 2015 crashes jedit tool on startup
- Peter Lammich, lammich@in.tum.de - Thu, 21 Jan 2016 13:18:21 +0000
- [isabelle] RC1: Immediate completion on \-symbols
- Peter Lammich, lammich@in.tum.de - Fri, 22 Jan 2016 16:30:39 +0000
- C. Diekmann, diekmann@in.tum.de - Fri, 22 Jan 2016 17:52:45 +0000
- Makarius, makarius@sketis.net - Fri, 22 Jan 2016 18:01:48 +0000
- Makarius, makarius@sketis.net - Fri, 22 Jan 2016 18:12:38 +0000
- Peter Lammich, lammich@in.tum.de - Fri, 22 Jan 2016 18:19:08 +0000
- Makarius, makarius@sketis.net - Fri, 22 Jan 2016 18:31:46 +0000
- Lawrence Paulson, lp15@cam.ac.uk - Fri, 22 Jan 2016 18:54:43 +0000
- Makarius, makarius@sketis.net - Fri, 22 Jan 2016 19:03:23 +0000
- Makarius, makarius@sketis.net - Fri, 22 Jan 2016 19:07:40 +0000
- Peter Lammich, lammich@in.tum.de - Fri, 22 Jan 2016 19:22:03 +0000
- Makarius, makarius@sketis.net - Fri, 22 Jan 2016 19:29:56 +0000
- Makarius, makarius@sketis.net - Sun, 24 Jan 2016 23:03:31 +0000
- [isabelle] RV 2016, Sept 23-30 2016, Madrid, Spain - 1st Call for Papers and Tutorials
- YliÃs Falcone, ylies.falcone@imag.fr - Fri, 15 Jan 2016 18:11:08 +0000
- Re: [isabelle] Short syntax for "solves <method>"
- Makarius, makarius@sketis.net - Sat, 09 Jan 2016 19:45:56 +0000
- [isabelle] simplifying functions on tuples
- Re: [isabelle] Sledgehammer: One-line proof reconstruction failed [still happening in RC2]
- Lars Hupel, hupel@in.tum.de - Fri, 29 Jan 2016 11:26:18 +0000
- [isabelle] SMT proof fails with exception
- Lars Hupel, hupel@in.tum.de - Fri, 29 Jan 2016 15:19:54 +0000
- Jasmin Blanchette, jasmin.blanchette@inria.fr - Fri, 29 Jan 2016 17:03:35 +0000
- [isabelle] subtype definition in Isabelle
- 刘涛, liut@ios.ac.cn - Fri, 15 Jan 2016 03:00:52 +0000
- Makarius, makarius@sketis.net - Sat, 16 Jan 2016 11:13:49 +0000
- [isabelle] Symbols: \<longleftrightarrow> vs. <->
- C. Diekmann, diekmann@in.tum.de - Thu, 21 Jan 2016 20:35:35 +0000
- Makarius, makarius@sketis.net - Thu, 21 Jan 2016 20:52:38 +0000
- C. Diekmann, diekmann@in.tum.de - Fri, 22 Jan 2016 08:47:50 +0000
- [isabelle] TAP (Tests and Proofs) 2016, final call for papers
- [isabelle] TERM exception in fologic.ML
- [isabelle] The violation of type restrictions by the Goedel numbering (or encoding) function
- Ken Kubota, mail@kenkubota.de - Mon, 04 Jan 2016 17:00:21 +0000
- [isabelle] Time for testing Isabelle2016-RC is now!
- Makarius, makarius@sketis.net - Fri, 22 Jan 2016 19:47:06 +0000
This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.