Cl-isabelle-users January 2016 Archives by subject

• January 2016 messages sorted by: [ thread ] [ author ] [ date ]
• More info on this list...
• List archive Table of Contents

• Re: [isabelle] Funny font metrics in the Search and Replace dialog [Isabelle2016-RC2]
  • Clemens Ballarin, ballarin@in.tum.de - Wed, 27 Jan 2016 19:48:54 +0000
  • Clemens Ballarin, ballarin@in.tum.de - Thu, 28 Jan 2016 18:21:56 +0000
  • Clemens Ballarin, ballarin@in.tum.de - Fri, 29 Jan 2016 19:11:04 +0000
  • Clemens Ballarin, ballarin@in.tum.de - Fri, 29 Jan 2016 23:08:51 +0000
• Re: [isabelle] "apply auto" transforms provable statement to something false?
  • Manuel Eberl, eberlm@in.tum.de - Mon, 25 Jan 2016 11:26:12 +0000
  • Andreas Lochbihler, andreas.lochbihler@inf.ethz.ch - Mon, 25 Jan 2016 11:28:25 +0000
  • Eugene W. Stark, isabelle-users@starkeffect.com - Mon, 25 Jan 2016 11:37:06 +0000
  • Lawrence Paulson, lp15@cam.ac.uk - Mon, 25 Jan 2016 11:58:00 +0000
• [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]
  • Clemens Ballarin, ballarin@in.tum.de - Tue, 26 Jan 2016 22:11:26 +0000
• 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?
  • Joachim Breitner, breitner@kit.edu - Tue, 05 Jan 2016 12:46:46 +0000
  • Dmitriy Traytel, traytel@inf.ethz.ch - Thu, 07 Jan 2016 10:02:09 +0000
  • Joachim Breitner, breitner@kit.edu - Thu, 07 Jan 2016 10:18:44 +0000
• [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)
  • Stephanie Schwartz, Stephanie.Schwartz@millersville.edu - Fri, 01 Jan 2016 19:31:02 +0000
• [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
  • C. Diekmann, diekmann@in.tum.de - Sun, 03 Jan 2016 18:01:31 +0000
  • Lawrence Paulson, lp15@cam.ac.uk - Sun, 03 Jan 2016 18:39:43 +0000
• [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
  • Makarius, makarius@sketis.net - Sat, 09 Jan 2016 15:00:35 +0000
  • Gottfried Barrow, igbi@gmx.com - Sun, 10 Jan 2016 17:12:10 +0000
  • Gottfried Barrow, igbi@gmx.com - Wed, 20 Jan 2016 00:55:58 +0000
• [isabelle] lift_bnf Subscript exception
  • Manuel Eberl, eberlm@in.tum.de - Mon, 11 Jan 2016 16:37:56 +0000
  • Dmitriy Traytel, traytel@inf.ethz.ch - Mon, 11 Jan 2016 20:52:05 +0000
  • Dmitriy Traytel, traytel@inf.ethz.ch - Tue, 12 Jan 2016 09:39:38 +0000
• [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
  • Lawrence Paulson, lp15@cam.ac.uk - Thu, 14 Jan 2016 15:44:29 +0000
• [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
  • W. Douglas Maurer, maurer@email.gwu.edu - Wed, 13 Jan 2016 23:04:30 +0000
• [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
  • Peter Lammich, lammich@in.tum.de - Thu, 21 Jan 2016 17:03:42 +0000
  • Dmitriy Traytel, traytel@inf.ethz.ch - Fri, 22 Jan 2016 10:09:13 +0000
• 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
  • Viorel Preoteasa, viorel.preoteasa@aalto.fi - Wed, 27 Jan 2016 09:54:24 +0000
• 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
  • Jasmin Blanchette, jasmin.blanchette@inria.fr - Mon, 18 Jan 2016 19:07:15 +0000
• [isabelle] TERM exception in fologic.ML
  • Slawomir Kolodynski via Cl-isabelle-users, cl-isabelle-users@lists.cam.ac.uk - Sat, 23 Jan 2016 17:20:52 +0000
  • Makarius, makarius@sketis.net - Sat, 23 Jan 2016 22:37:04 +0000
• [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