Cl-isabelle-users November 2020 Archives by date

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

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