Cl-isabelle-users November 2020 Archives by subject

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

• [isabelle] Another Issue with Isabelle/jEdit with macOS Big Sur
  • Lawrence Paulson, lp15 at cam.ac.uk - Thu, 19 Nov 2020 16:31:16 +0000
  • Makarius, makarius at sketis.net - Thu, 19 Nov 2020 16:39:52 +0000
  • Lawrence Paulson, lp15 at cam.ac.uk - Thu, 19 Nov 2020 16:42:01 +0000
  • Makarius, makarius at sketis.net - Fri, 20 Nov 2020 10:58:58 +0000
  • Lawrence Paulson, lp15 at cam.ac.uk - Fri, 20 Nov 2020 11:06:41 +0000
• [isabelle] AutoCorres 1.7 and CParser 1.17 for Isabelle2020
  • Klein, Gerwin (Data61, Kensington NSW), Gerwin.Klein at data61.csiro.au - Tue, 10 Nov 2020 02:20:08 +0000
• [isabelle] Bug? Or still just confusing correct behavior?
  • Peter Reitinger, peter.reitinger at gmail.com - Sat, 21 Nov 2020 05:24:49 +0000
• [isabelle] Bug report Isabelle 2019 and Isabelle 2020
  • Peter Reitinger, peter.reitinger at gmail.com - Sat, 21 Nov 2020 05:56:36 +0000
  • Makarius, makarius at sketis.net - Sat, 21 Nov 2020 12:02:51 +0000
  • Peter Reitinger, peter.reitinger at gmail.com - Mon, 23 Nov 2020 03:23:27 +0000
  • Manuel Eberl, eberlm at in.tum.de - Mon, 23 Nov 2020 07:48:52 +0000
  • Mathias Fleury, mathias.fleury12 at gmail.com - Mon, 23 Nov 2020 08:14:41 +0000
  • Mathias Fleury, mathias.fleury12 at gmail.com - Mon, 23 Nov 2020 10:12:45 +0000
• [isabelle] Call for Papers - SPIN 2021
  • Laarman, A.W., a.w.laarman at liacs.leidenuniv.nl - Fri, 06 Nov 2020 12:11:11 +0000
• [isabelle] Code generation for non-terminating functions
  • David Kretzmer, david.k at posteo.de - Tue, 17 Nov 2020 18:12:21 +0000
  • Thiemann, René, Rene.Thiemann at uibk.ac.at - Tue, 17 Nov 2020 18:47:24 +0000
  • David Kretzmer, david.k at posteo.de - Tue, 17 Nov 2020 19:56:45 +0000
• [isabelle] Code generation: transitive closure of inductive predicate does not terminate
  • David Kretzmer, david.k at posteo.de - Tue, 03 Nov 2020 17:24:58 +0000
  • Lukas Bulwahn, lukas.bulwahn at gmail.com - Wed, 04 Nov 2020 11:35:10 +0000
  • David Kretzmer, david.k at posteo.de - Wed, 04 Nov 2020 14:50:07 +0000
  • Andreas Lochbihler, mail at andreas-lochbihler.de - Wed, 04 Nov 2020 19:56:31 +0000
  • David Kretzmer, david.k at posteo.de - Wed, 04 Nov 2020 20:21:15 +0000
• [isabelle] Codegen for List.member overwrites List structure in SML
  • David Kretzmer, david.k at posteo.de - Tue, 10 Nov 2020 10:00:56 +0000
• Re: [isabelle] Codegen for List.member overwrites List structure in SML
  • David Kretzmer, david.k at posteo.de - Tue, 10 Nov 2020 19:57:40 +0000
  • Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de - Thu, 12 Nov 2020 08:27:48 +0000
• [isabelle] Counting lines of code/definition vs proof?
  • Jason Gross, jasongross9 at gmail.com - Sat, 14 Nov 2020 04:11:02 +0000
  • Makarius, makarius at sketis.net - Thu, 19 Nov 2020 13:55:05 +0000
• [isabelle] Definitional axioms in Isabelle/ML?
  • Mikhail Chekhov, mikhail.chekhov.w at gmail.com - Sat, 07 Nov 2020 18:09:34 +0000
  • Mikhail Chekhov, mikhail.chekhov.w at gmail.com - Sat, 07 Nov 2020 19:11:26 +0000
• [isabelle] Document preparation from within Isabelle/jEdit
  • David Kretzmer, david.k at posteo.de - Fri, 06 Nov 2020 16:59:24 +0000
  • Makarius, makarius at sketis.net - Fri, 06 Nov 2020 20:59:20 +0000
  • David Kretzmer, david.k at posteo.de - Fri, 06 Nov 2020 22:16:39 +0000
  • Makarius, makarius at sketis.net - Fri, 06 Nov 2020 22:29:06 +0000
  • David Kretzmer, david.k at posteo.de - Fri, 06 Nov 2020 22:50:28 +0000
• [isabelle] Final Deadline - Survey on the AFP
  • MACKENZIE Carlin, s1724780 at sms.ed.ac.uk - Mon, 30 Nov 2020 11:30:21 +0000
• [isabelle] FSCD 2021: First Call for Papers
  • Carsten Fuhs, carsten at dcs.bbk.ac.uk - Fri, 06 Nov 2020 13:32:09 +0000
• [isabelle] fully funded PhD position at University of Sheffield on the formal verification of industrial robots
  • Andrei Popescu, andrei.h.popescu at gmail.com - Mon, 30 Nov 2020 10:00:45 +0000
• [isabelle] General timeout for tactics
  • Max Haslbeck, max.haslbeck at gmx.de - Tue, 03 Nov 2020 12:15:54 +0000
  • Mikhail Chekhov, mikhail.chekhov.w at gmail.com - Tue, 03 Nov 2020 12:43:13 +0000
  • Manuel Eberl, eberlm at in.tum.de - Tue, 03 Nov 2020 12:48:31 +0000
  • Freek Wiedijk, freek at cs.ru.nl - Tue, 03 Nov 2020 13:44:15 +0000
  • Mikhail Chekhov, mikhail.chekhov.w at gmail.com - Tue, 03 Nov 2020 15:04:04 +0000
  • Mikhail Chekhov, mikhail.chekhov.w at gmail.com - Tue, 03 Nov 2020 19:57:59 +0000
  • Thomas Sewell, tals4 at cam.ac.uk - Wed, 04 Nov 2020 11:39:59 +0000
  • Mikhail Chekhov, mikhail.chekhov.w at gmail.com - Wed, 04 Nov 2020 19:09:05 +0000
  • Manuel Eberl, eberlm at in.tum.de - Wed, 04 Nov 2020 19:17:41 +0000
• Re: [isabelle] How do I set --maxheap greater than 16G on Linux?
  • Makarius, makarius at sketis.net - Sat, 07 Nov 2020 21:14:18 +0000
  • Eugene W. Stark, isabelle-users at starkeffect.com - Sat, 07 Nov 2020 22:14:28 +0000
• Re: [isabelle] Implicit exporting of goal state by different commands (done, by, qed)
  • Makarius, makarius at sketis.net - Sat, 07 Nov 2020 21:09:37 +0000
  • Mikhail Mandrykin, mandrykin at ispras.ru - Sat, 07 Nov 2020 22:33:43 +0000
  • Mikhail Mandrykin, mandrykin at ispras.ru - Sat, 07 Nov 2020 22:53:50 +0000
  • Makarius, makarius at sketis.net - Sat, 07 Nov 2020 23:02:53 +0000
  • Buday Gergely via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk - Mon, 09 Nov 2020 09:29:35 +0000
  • Mikhail Mandrykin, mandrykin at ispras.ru - Mon, 09 Nov 2020 16:22:36 +0000
• Re: [isabelle] Improvement suggestion for isabelle process
  • Makarius, makarius at sketis.net - Sat, 07 Nov 2020 16:31:18 +0000
• [isabelle] Isabelle2021-RC0 available for early experiments
  • Makarius, makarius at sketis.net - Mon, 30 Nov 2020 12:53:18 +0000
• [isabelle] Issue with Isabelle/jEdit in fullscreen mode in macOS Big Sur
  • Norbert Schirmer via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk - Mon, 16 Nov 2020 07:58:51 +0000
• [isabelle] ITP 2021 : Second Call for Papers
  • Liron Cohen, cliron at bgu.ac.il - Sun, 29 Nov 2020 14:23:37 +0000
• [isabelle] Local varification/unvarification in Isabelle/ML?
  • Mikhail Chekhov, mikhail.chekhov.w at gmail.com - Wed, 18 Nov 2020 00:08:46 +0000
• [isabelle] Looking for partner to teach course on Isabelle for talented German high school students
  • Luckhardt, Daniel, daniel.luckhardt at mathematik.uni-goettingen.de - Tue, 24 Nov 2020 02:28:41 +0000
• [isabelle] Manually using a SideKick parser
  • MACKENZIE Carlin, s1724780 at sms.ed.ac.uk - Wed, 18 Nov 2020 12:28:55 +0000
  • Makarius, makarius at sketis.net - Thu, 19 Nov 2020 11:47:05 +0000
• [isabelle] NASA Formal Methods Symposium (NFM2021) -- Final CFP (Extended Deadline)
  • Moscato, Mariano M. (LARC-D320)[NATIONAL INSTITUTE OF AEROSPACE] via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk - Fri, 27 Nov 2020 12:54:33 +0000
• [isabelle] new in the AFP
  • Lawrence Paulson, lp15 at cam.ac.uk - Fri, 27 Nov 2020 14:10:20 +0000
• [isabelle] New in the AFP: AI planning
  • Lawrence Paulson, lp15 at cam.ac.uk - Fri, 13 Nov 2020 13:24:02 +0000
• [isabelle] New in the AFP: Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information
  • Thiemann, René, Rene.Thiemann at uibk.ac.at - Mon, 30 Nov 2020 09:09:44 +0000
• [isabelle] NFM2021 - Second Call for Papers
  • Moscato, Mariano M. (LARC-D320)[NATIONAL INSTITUTE OF AEROSPACE] via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk - Fri, 13 Nov 2020 13:37:29 +0000
• [isabelle] Observations on ZF
  • Pedro Sánchez Terraf, sterraf at famaf.unc.edu.ar - Sat, 28 Nov 2020 21:28:34 +0000
  • Makarius, makarius at sketis.net - Sun, 29 Nov 2020 12:20:01 +0000
  • Pedro Sánchez Terraf, sterraf at famaf.unc.edu.ar - Sun, 29 Nov 2020 12:33:38 +0000
  • Makarius, makarius at sketis.net - Sun, 29 Nov 2020 12:48:43 +0000
  • Lawrence Paulson, lp15 at cam.ac.uk - Mon, 30 Nov 2020 10:32:18 +0000
• [isabelle] pat_completeness exception
  • Tobias Nipkow, nipkow at in.tum.de - Tue, 03 Nov 2020 12:49:45 +0000
• [isabelle] Pretty-printing primed identifiers
  • Tobias Nipkow, nipkow at in.tum.de - Thu, 26 Nov 2020 11:28:18 +0000
• [isabelle] Question about "try" and future tasks
  • Eugene W. Stark, isabelle-users at starkeffect.com - Thu, 19 Nov 2020 00:49:29 +0000
• [isabelle] ROOT file for imported theory
  • Buday Gergely via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk - Thu, 12 Nov 2020 14:12:17 +0000
  • Jakub Kądziołka, kuba at kadziolka.net - Thu, 12 Nov 2020 14:36:40 +0000
  • Buday Gergely via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk - Fri, 13 Nov 2020 07:17:26 +0000
• [isabelle] scala-isabelle: A library for interfacing with Isabelle from Scala (or Java)
  • Dominique Unruh, unruh at ut.ee - Thu, 12 Nov 2020 13:22:58 +0000
• [isabelle] State of affairs with words
  • Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de - Mon, 30 Nov 2020 18:57:05 +0000
• [isabelle] Sub/superscripts in document preparation
  • Pedro Sánchez Terraf, sterraf at famaf.unc.edu.ar - Mon, 30 Nov 2020 14:23:45 +0000
• [isabelle] superfluous assumptions in comm_append_are_replicate
  • Stepan Holub, holub at karlin.mff.cuni.cz - Thu, 26 Nov 2020 12:52:36 +0000
  • Lawrence Paulson, lp15 at cam.ac.uk - Thu, 26 Nov 2020 18:10:24 +0000
  • Tobias Nipkow, nipkow at in.tum.de - Thu, 26 Nov 2020 18:31:34 +0000
• [isabelle] Survey on the AFP
  • MACKENZIE Carlin, s1724780 at sms.ed.ac.uk - Tue, 10 Nov 2020 15:26:50 +0000
• [isabelle] two proof-assistant friendly posts of Lecturer in Cybersecurity at University of Sheffield: deadline 3rd December 2020
  • Andrei Popescu, andrei.h.popescu at gmail.com - Fri, 20 Nov 2020 13:11:07 +0000
• [isabelle] Typos in lemma names
  • Jakub Kądziołka, kuba at kadziolka.net - Sat, 14 Nov 2020 11:41:35 +0000
  • Lawrence Paulson, lp15 at cam.ac.uk - Sun, 15 Nov 2020 14:02:11 +0000
• [isabelle] Unknown JAVA_HOME -- Java unavailable
  • Kawin Worrasangasilpa, kw448 at cam.ac.uk - Mon, 30 Nov 2020 12:12:15 +0000
  • Makarius, makarius at sketis.net - Mon, 30 Nov 2020 13:06:07 +0000
• [isabelle] Weak lemma: HOL-Algebra.Multiplicative_Group.generate_pow_card
  • Jakub Kądziołka, kuba at kadziolka.net - Fri, 13 Nov 2020 18:29:37 +0000
  • Jakub Kądziołka, kuba at kadziolka.net - Fri, 13 Nov 2020 18:35:59 +0000