Cl-isabelle-users November 2020 Archives by subject
- [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
- [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
- [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
- [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)
- [isabelle] new in the AFP
- [isabelle] New in the AFP: AI planning
- [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
- [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
- [isabelle] scala-isabelle: A library for interfacing with Isabelle from Scala (or Java)
- [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
- [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
- [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
- [isabelle] Unknown JAVA_HOME -- Java unavailable
- [isabelle] Weak lemma: HOL-Algebra.Multiplicative_Group.generate_pow_card
This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.