Cl-isabelle-users February 2021 Archives by date

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

• Mon, 01 Feb 2021
  • [isabelle] New in the AFP: a port of GeoCoq - Lawrence Paulson, lp15 at cam.ac.uk
  • [isabelle] Isabelle2021-RC4 available for applications - Makarius, makarius at sketis.net
  • Re: [isabelle] Isabelle2021-RC4: bundling of Naproche-SAD - Makarius, makarius at sketis.net
  • Re: [isabelle] Isabelle2021-RC2: slight regression in HTML output - Makarius, makarius at sketis.net
  • Re: [isabelle] Isabelle2021-RC3: Java 11 (LTS) vs. Java 15 (MTS) - Makarius, makarius at sketis.net
  • Re: [isabelle] Isabelle2021-RC0: Java/VM monitor - Makarius, makarius at sketis.net
  • Re: [isabelle] Isabelle2021-RC0: Java/VM monitor - Eugene W. Stark, isabelle-users at starkeffect.com
  • [isabelle] New in the AFP: Solution to the xkcd Blue Eyes puzzle - Manuel Eberl, eberlm at in.tum.de
  • [isabelle] Isabelle logo terms of use - Stepan Holub, holub at karlin.mff.cuni.cz
• Tue, 02 Feb 2021
  • [isabelle] Call for Papers: Tests and Proofs 2021 (TAP 2021) New Deadlines - Frederic Loulergue, frederic.loulergue at univ-orleans.fr
  • [isabelle] CfP: SCSS 2021 - Temur Kutsia, kutsia at risc.jku.at
  • Re: [isabelle] Isabelle logo terms of use - Makarius, makarius at sketis.net
• Wed, 03 Feb 2021
  • Re: [isabelle] Isabelle code for getting in-memory representation (abstract syntax trees) for complete theory file (tree of loaded theories) - Makarius, makarius at sketis.net
• Thu, 04 Feb 2021
  • Re: [isabelle] Isabelle2021-RC1 - Any way to limit "veriT" memory use? - Jasmin Blanchette via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk
  • Re: [isabelle] Isabelle2021-RC1 - Any way to limit "veriT" memory use? - Dominique Unruh, unruh at ut.ee
• Fri, 05 Feb 2021
  • [isabelle] Rewrites for a sublocale with UNIV as the carrier set - Lukas Stevens, lukas.stevens+isabelle-users at in.tum.de
  • [isabelle] Incompatibility between code generation, HOL-Library.Numeral_Type, and Containers.Set_Impl - Dominique Unruh, unruh at ut.ee
  • Re: [isabelle] Isabelle2021-RC1 - Any way to limit "veriT" memory use? - Makarius, makarius at sketis.net
  • Re: [isabelle] Isabelle code for getting in-memory representation (abstract syntax trees) for complete theory file (tree of loaded theories) - Wenda Li, wl302 at cam.ac.uk
  • Re: [isabelle] Isabelle code for getting in-memory representation (abstract syntax trees) for complete theory file (tree of loaded theories) - Makarius, makarius at sketis.net
  • Re: [isabelle] Isabelle code for getting in-memory representation (abstract syntax trees) for complete theory file (tree of loaded theories) - Wenda Li, wl302 at cam.ac.uk
  • [isabelle] Atb.: Isabelle code for getting in-memory representation (abstract syntax trees) for complete theory file (tree of loaded theories) - Alex Meyer, alex153 at outlook.lv
• Sun, 07 Feb 2021
  • Re: [isabelle] Rewrites for a sublocale with UNIV as the carrier set - YAMADA, Akihisa, ayamada at trs.cm.is.nagoya-u.ac.jp
• Mon, 08 Feb 2021
  • Re: [isabelle] Rewrites for a sublocale with UNIV as the carrier set - Lukas Stevens, lukas.stevens+isabelle-users at in.tum.de
  • Re: [isabelle] Rewrites for a sublocale with UNIV as the carrier set - YAMADA, Akihisa, ayamada at trs.cm.is.nagoya-u.ac.jp
  • Re: [isabelle] Rewrites for a sublocale with UNIV as the carrier set - Mikhail Chekhov, mikhail.chekhov.w at gmail.com
  • [isabelle] Isabelle2021-RC5 available for applications - Makarius, makarius at sketis.net
  • Re: [isabelle] Isabelle2021-RC5: support for Apple Silicon - Makarius, makarius at sketis.net
• Tue, 09 Feb 2021
  • [isabelle] 21st Midlands Graduate School in the Foundations of Computing Science: Call for Participation - Andrei Popescu, andrei.h.popescu at gmail.com
  • [isabelle] Comparing Isabelle/Scala with scala-isabelle. Was: Isabelle code for getting in-memory representation (abstract syntax trees) for complete theory file (tree of loaded theories) - Dominique Unruh, unruh at ut.ee
  • Re: [isabelle] Comparing Isabelle/Scala with scala-isabelle. Was: Isabelle code for getting in-memory representation (abstract syntax trees) for complete theory file (tree of loaded theories) - Makarius, makarius at sketis.net
  • Re: [isabelle] Comparing Isabelle/Scala with scala-isabelle. Was: Isabelle code for getting in-memory representation (abstract syntax trees) for complete theory file (tree of loaded theories) - Makarius, makarius at sketis.net
• Wed, 10 Feb 2021
  • [isabelle] Boolos's Curious Inference (Speed-Up) in Isabelle/HOL - Jeffrey Ketland, jeffreyketland at gmail.com
  • Re: [isabelle] Boolos's Curious Inference (Speed-Up) in Isabelle/HOL - Jakub Kądziołka, kuba at kadziolka.net
  • [isabelle] Syntax proposal: multiway if - Manuel Eberl, eberlm at in.tum.de
  • Re: [isabelle] Syntax proposal: multiway if - Peter Lammich, lammich at in.tum.de
  • Re: [isabelle] Syntax proposal: multiway if - Manuel Eberl, eberlm at in.tum.de
  • Re: [isabelle] Syntax proposal: multiway if - Christian Sternagel, c.sternagel at gmail.com
  • Re: [isabelle] Syntax proposal: multiway if - Manuel Eberl, eberlm at in.tum.de
  • Re: [isabelle] Syntax proposal: multiway if - Gerwin Klein, kleing at unsw.edu.au
• Thu, 11 Feb 2021
  • [isabelle] New in the AFP: The Laws of Large Numbers - Gerwin Klein, kleing at unsw.edu.au
  • [isabelle] FSCD 2021: Extended deadline (Abstract: February 16/ Submission: February 22) - Carsten Fuhs, carsten at dcs.bbk.ac.uk
  • [isabelle] PhD position in Formal Methods/Decompilation at the Open University of The Netherlands - Freek Verbeek, freek at vt.edu
  • Re: [isabelle] Comparing Isabelle/Scala with scala-isabelle. Was: Isabelle code for getting in-memory representation (abstract syntax trees) for complete theory file (tree of loaded theories) - Dominique Unruh, unruh at ut.ee
  • Re: [isabelle] Comparing Isabelle/Scala with scala-isabelle. Was: Isabelle code for getting in-memory representation (abstract syntax trees) for complete theory file (tree of loaded theories) - Makarius, makarius at sketis.net
  • Re: [isabelle] isabelle scala_project and Gradle / IntelliJ support - Makarius, makarius at sketis.net
  • [isabelle] CFP SAT-2021: Deadline March 19th - Jesús Giráldez Crú, jgiraldez at ugr.es
• Fri, 12 Feb 2021
  • [isabelle] RC5: Sledgehammer and HOL-Library.Word problems - Peter Lammich, lammich at in.tum.de
  • Re: [isabelle] RC5: Sledgehammer and HOL-Library.Word problems - Mathias Fleury, mathias.fleury12 at gmail.com
  • [isabelle] RC5: Syntactic class bit_operations is gone - Peter Lammich, lammich at in.tum.de
  • [isabelle] RC5: Short experience report - Peter Lammich, lammich at in.tum.de
  • Re: [isabelle] RC5: Syntactic class bit_operations is gone - Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de
  • Re: [isabelle] RC5: Syntactic class bit_operations is gone - Peter Lammich, lammich at in.tum.de
• Sat, 13 Feb 2021
  • Re: [isabelle] RC5: Syntactic class bit_operations is gone - Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de
  • Re: [isabelle] RC5: Syntactic class bit_operations is gone - Peter Lammich, lammich at in.tum.de
  • [isabelle] Some more polishing of the multiset theory - Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de
  • Re: [isabelle] Some more polishing of the multiset theory - Manuel Eberl, eberlm at in.tum.de
  • Re: [isabelle] Isabelle2021-RC5: support for Apple Silicon - Makarius, makarius at sketis.net
  • Re: [isabelle] Isabelle2021-RC3 New failure mode for "try"/sledgehammer - Eugene W. Stark, isabelle-users at starkeffect.com
  • Re: [isabelle] Rewrites for a sublocale with UNIV as the carrier set - Clemens Ballarin, ballarin at in.tum.de
• Sun, 14 Feb 2021
  • [isabelle] Weird nesting of Quantifiers - Peter Lammich, lammich at in.tum.de
  • Re: [isabelle] Some more polishing of the multiset theory - Tobias Nipkow, nipkow at in.tum.de
  • Re: [isabelle] Weird nesting of Quantifiers - Tobias Nipkow, nipkow at in.tum.de
  • [isabelle] Isabelle2021-RC6 available for applications - Makarius, makarius at sketis.net
• Mon, 15 Feb 2021
  • Re: [isabelle] RC5: Short experience report - Jasmin Blanchette via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk
  • Re: [isabelle] RC5: Sledgehammer and HOL-Library.Word problems - Thomas Sewell, tals4 at cam.ac.uk
  • Re: [isabelle] Weird nesting of Quantifiers - Thomas Sewell, tals4 at cam.ac.uk
  • Re: [isabelle] Weird nesting of Quantifiers - Lawrence Paulson, lp15 at cam.ac.uk
  • Re: [isabelle] RC5: Short experience report - Lawrence Paulson, lp15 at cam.ac.uk
  • Re: [isabelle] RC5: Short experience report - Tobias Nipkow, nipkow at in.tum.de
• Tue, 16 Feb 2021
  • [isabelle] Open pdf files from Isabelle File Browser - Peter Koepke, koepke at math.uni-bonn.de
  • Re: [isabelle] Isabelle2021-RC3 New failure mode for "try"/sledgehammer - Mathias Fleury, mathias.fleury12 at gmail.com
  • Re: [isabelle] Open pdf files from Isabelle File Browser - Makarius, makarius at sketis.net
  • Re: [isabelle] Isabelle2021-RC3 New failure mode for "try"/sledgehammer - Makarius, makarius at sketis.net
  • Re: [isabelle] Rewrites for a sublocale with UNIV as the carrier set - Lukas Stevens, lukas.stevens+isabelle-users at in.tum.de
  • Re: [isabelle] Isabelle2021-RC3 New failure mode for "try"/sledgehammer - Eugene W. Stark, isabelle-users at starkeffect.com
  • Re: [isabelle] Weird nesting of Quantifiers - Peter Lammich, lammich at in.tum.de
  • [isabelle] Conflict of type arities: What are the constraints on class instantiations? - Peter Lammich, lammich at in.tum.de
  • Re: [isabelle] Conflict of type arities: What are the constraints on class instantiations? - Tobias Nipkow, nipkow at in.tum.de
  • Re: [isabelle] Isabelle2021-RC3 New failure mode for "try"/sledgehammer - Mathias Fleury, mathias.fleury12 at gmail.com
  • [isabelle] Assistant/Associate Professor positions in Edinburgh, UK (Herio-Watt University): Logic, Programming Languages, Verification, Security - Ekaterina Komendantskaya, komendantskaya at gmail.com
  • Re: [isabelle] Conflict of type arities: What are the constraints on class instantiations? - Jakub Kądziołka, kuba at kadziolka.net
• Wed, 17 Feb 2021
  • Re: [isabelle] Conflict of type arities: What are the constraints on class instantiations? - Jeremy Dawson, Jeremy.Dawson at anu.edu.au
  • [isabelle] Yet another Isabelle-Course available - Burkhart Wolff, wolff at lri.fr
• Fri, 19 Feb 2021
  • [isabelle] Predicate Compiler fails with "No specification for ..." - Florian Märkl, isabelle-users at florianmaerkl.de
  • [isabelle] unused_thms in composed theorems - Stepan Holub, holub at karlin.mff.cuni.cz
  • Re: [isabelle] Syntax proposal: multiway if - Mikhail Chekhov, mikhail.chekhov.w at gmail.com
  • Re: [isabelle] Syntax proposal: multiway if - Manuel Eberl, eberlm at in.tum.de
  • [isabelle] 2nd CfP ThEdu'21 - Walther Neuper, walther.neuper at jku.at
  • [isabelle] Relation of function absent from Main - Christian Pardillo Laursen, cp735 at cam.ac.uk
• Sat, 20 Feb 2021
  • [isabelle] 14th Conference on Intelligent Computer Mathematics (CICM 2021), Invited Speakers Update & Second call for papers, Conference Date: July 26-31, 2021 - Serge Autexier, serge.autexier at dfki.de
  • Re: [isabelle] Predicate Compiler fails with "No specification for ..." - Tobias Nipkow, nipkow at in.tum.de
  • Re: [isabelle] Relation of function absent from Main - Tobias Nipkow, nipkow at in.tum.de
  • [isabelle] Request for TTP and PTT Interfaces - Jens-D. Doll, jens.doll at live.de
  • [isabelle] First day with HOL/Isabelle - McCue, Brian, brian.mccue at snhu.edu
  • Re: [isabelle] Predicate Compiler fails with "No specification for ..." - Florian Märkl, isabelle-users at florianmaerkl.de
  • Re: [isabelle] Relation of function absent from Main - Dmitriy Traytel, traytel at di.ku.dk
• Sun, 21 Feb 2021
  • Re: [isabelle] Predicate Compiler fails with "No specification for ..." - Andreas Lochbihler, mail at andreas-lochbihler.de
  • Re: [isabelle] First day with HOL/Isabelle - C. Diekmann, diekmann at in.tum.de
  • Re: [isabelle] Predicate Compiler fails with "No specification for ..." - Florian Märkl, isabelle-users at florianmaerkl.de
  • Re: [isabelle] First day with HOL/Isabelle - Jakub Kądziołka, kuba at kadziolka.net
  • Re: [isabelle] Predicate Compiler fails with "No specification for ..." - Andreas Lochbihler, mail at andreas-lochbihler.de
  • Re: [isabelle] First day with HOL/Isabelle - Thomas Sewell, tals4 at cam.ac.uk
  • [isabelle] Announcing Isabelle2021 - Makarius, makarius at sketis.net
• Mon, 22 Feb 2021
  • [isabelle] Unfixed variables in "define" command - Manuel Eberl, eberlm at in.tum.de
  • Re: [isabelle] Unfixed variables in "define" command - Makarius, makarius at sketis.net
  • Re: [isabelle] Unfixed variables in "define" command - Jakub Kądziołka, kuba at kadziolka.net
  • Re: [isabelle] Unfixed variables in "define" command - Makarius, makarius at sketis.net
  • Re: [isabelle] Unfixed variables in "define" command - Manuel Eberl, eberlm at in.tum.de
  • Re: [isabelle] Unfixed variables in "define" command - Makarius, makarius at sketis.net
  • Re: [isabelle] Unfixed variables in "define" command - Makarius, makarius at sketis.net
• Tue, 23 Feb 2021
  • [isabelle] AFP 2021 - Gerwin Klein, kleing at unsw.edu.au
  • Re: [isabelle] AFP 2021 - Makarius, makarius at sketis.net
  • Re: [isabelle] Request for TTP and PTT Interfaces - Makarius, makarius at sketis.net
  • [isabelle] Berghofer's program extraction mechanism and code generation - Dr A. Koutsoukou-Argyraki, ak2110 at cam.ac.uk
  • Re: [isabelle] Berghofer's program extraction mechanism and code generation - Manuel Eberl, eberlm at in.tum.de
• Wed, 24 Feb 2021
  • Re: [isabelle] Berghofer's program extraction mechanism and code generation - Tjark Weber, tjark.weber at it.uu.se
  • [isabelle] Error in DockerHub documentation - Boris Shminke via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk
  • [isabelle] Bill McCune PhD Award in Automated Reasoning, Call for Nominations - Pascal Fontaine, Pascal.Fontaine at inria.fr
  • [isabelle] New in the AFP: Formal Puiseux Series - Lawrence Paulson, lp15 at cam.ac.uk
  • Re: [isabelle] New in the AFP: Formal Puiseux Series - Manuel Eberl, eberlm at in.tum.de
  • Re: [isabelle] New in the AFP: Formal Puiseux Series - Wenda Li, wl302 at cam.ac.uk
  • Re: [isabelle] New in the AFP: Formal Puiseux Series - Manuel Eberl, eberlm at in.tum.de
  • Re: [isabelle] New in the AFP: Formal Puiseux Series - Freek Wiedijk, freek at cs.ru.nl
  • [isabelle] AFP instructions - Stepan Holub, holub at karlin.mff.cuni.cz
  • Re: [isabelle] Error in DockerHub documentation - Makarius, makarius at sketis.net
  • Re: [isabelle] AFP instructions - Makarius, makarius at sketis.net
  • Re: [isabelle] AFP instructions - Stepan Holub, holub at karlin.mff.cuni.cz
  • Re: [isabelle] Error in DockerHub documentation - Boris Shminke via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk
  • Re: [isabelle] Error in DockerHub documentation - Makarius, makarius at sketis.net
  • [isabelle] F-IDE 2021 - Last Call for Papers - Extended Deadline - Andrei Paskevich, andrei.paskevich at lri.fr
  • Re: [isabelle] AFP instructions - Gerwin Klein, kleing at unsw.edu.au
  • Re: [isabelle] AFP instructions - Fernandez, Matthew, matthew.fernandez at intel.com
  • Re: [isabelle] AFP instructions - Gerwin Klein, kleing at unsw.edu.au
• Thu, 25 Feb 2021
  • Re: [isabelle] AFP instructions - Stepan Holub, holub at karlin.mff.cuni.cz
  • Re: [isabelle] Error in DockerHub documentation - Boris Shminke via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk
  • Re: [isabelle] AFP instructions - Gerwin Klein, kleing at unsw.edu.au
  • Re: [isabelle] AFP instructions - Makarius, makarius at sketis.net
  • Re: [isabelle] AFP instructions - Makarius, makarius at sketis.net
  • [isabelle] Postdoc/phd positions in ERC project "Certified Quantum Security" (formal verification of quantum crypto) - Dominique Unruh, unruh at ut.ee
  • [isabelle] FMCAD 2021: First Call for Papers - Michael Whalen via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk
  • Re: [isabelle] Berghofer's program extraction mechanism and code generation - Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de
  • Re: [isabelle] RC5: Syntactic class bit_operations is gone - Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de
  • Re: [isabelle] Weak lemma: HOL-Algebra.Multiplicative_Group.generate_pow_card - Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de
  • Re: [isabelle] AFP instructions - Fernandez, Matthew, matthew.fernandez at intel.com
  • Re: [isabelle] AFP instructions - David Cock, david.cock at inf.ethz.ch
  • Re: [isabelle] AFP instructions - Gerwin Klein, kleing at unsw.edu.au
• Fri, 26 Feb 2021
  • Re: [isabelle] AFP instructions - Gerwin Klein, kleing at unsw.edu.au
  • [isabelle] New in the AFP: A Verified Imperative Implementation of B-Trees - Gerwin Klein, kleing at unsw.edu.au
  • [isabelle] Nitpick Codatatype - No Counterexample found - Stüber, Sebastian, stueber at se-rwth.de
  • Re: [isabelle] New in the AFP: Formal Puiseux Series - Manuel Eberl, eberlm at in.tum.de
  • Re: [isabelle] New in the AFP: Formal Puiseux Series - Manuel Eberl, eberlm at in.tum.de
  • [isabelle] Python client to Isabelle server - Boris Shminke via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk
  • Re: [isabelle] New in the AFP: Formal Puiseux Series - Mohammad Abdulaziz, mohammad.abdulaziz8 at gmail.com
  • Re: [isabelle] New in the AFP: Formal Puiseux Series - Manuel Eberl, eberlm at in.tum.de
  • Re: [isabelle] New in the AFP: Formal Puiseux Series - Manuel Eberl, eberlm at in.tum.de
  • Re: [isabelle] New in the AFP: Formal Puiseux Series - Mohammad Abdulaziz, mohammad.abdulaziz8 at gmail.com
  • Re: [isabelle] New in the AFP: Formal Puiseux Series - Freek Wiedijk, freek at cs.ru.nl
• Sat, 27 Feb 2021
  • Re: [isabelle] AFP instructions - Stepan Holub, holub at karlin.mff.cuni.cz
  • Re: [isabelle] AFP instructions - Makarius, makarius at sketis.net
  • Re: [isabelle] AFP instructions - Makarius, makarius at sketis.net
  • Re: [isabelle] AFP instructions - Stepan Holub, holub at karlin.mff.cuni.cz
  • Re: [isabelle] AFP instructions - Makarius, makarius at sketis.net
  • [isabelle] FMBC 2021: First Call for Papers - Marmsoler, Diego, D.Marmsoler at exeter.ac.uk
  • [isabelle] Remaining uses of "isabelle process" and "isabelle console" - Makarius, makarius at sketis.net
• Sun, 28 Feb 2021
  • [isabelle] SMT 2021 Workshop: Second Call for Papers - Nadel, Alexander, alexander.nadel at intel.com
  • Re: [isabelle] Error in DockerHub documentation - Makarius, makarius at sketis.net
  • Re: [isabelle] AFP instructions - Gerwin Klein, kleing at unsw.edu.au