Cl-isabelle-users March 2021 Archives by date

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

• Mon, 01 Mar 2021
  • Re: [isabelle] Remaining uses of "isabelle process" and "isabelle console" - Dominique Unruh, unruh at ut.ee
  • [isabelle] build output - Tobias Nipkow, nipkow at in.tum.de
  • Re: [isabelle] Error in DockerHub documentation - Boris Shminke via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk
  • [isabelle] New in the AFP: The Sunflower Lemma of Erdős and Rado - Tobias Nipkow, nipkow at in.tum.de
  • Re: [isabelle] Remaining uses of "isabelle process" and "isabelle console" - Makarius, makarius at sketis.net
  • Re: [isabelle] Python client to Isabelle server - Makarius, makarius at sketis.net
  • Re: [isabelle] Error in DockerHub documentation - Makarius, makarius at sketis.net
• Tue, 02 Mar 2021
  • [isabelle] VS Code extension - Jeremy Sylvestre, jsylvest at ualberta.ca
  • [isabelle] Working with list symmetry (Attributes for theory-specific theorem transformations?) - Martin Raška, RaskaMartin at seznam.cz
  • Re: [isabelle] VS Code extension - Makarius, makarius at sketis.net
  • [isabelle] Code generation for a subtype with free_constructors - Lukas Stevens, lukas.stevens+isabelle-users at in.tum.de
  • [isabelle] Fixing type variables in locales - Wolfgang Jeltsch, wolfgang-it at jeltsch.info
  • Re: [isabelle] Fixing type variables in locales - Christian Sternagel, c.sternagel at gmail.com
  • Re: [isabelle] Python client to Isabelle server - Boris Shminke via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk
  • Re: [isabelle] Fixing type variables in locales - Thiemann, René, Rene.Thiemann at uibk.ac.at
  • Re: [isabelle] Fixing type variables in locales - Wolfgang Jeltsch, wolfgang-it at jeltsch.info
  • [isabelle] Nitpick finds counterexample to proven lemma - Sander van Rijnswou, svanrijnswou at gmail.com
  • Re: [isabelle] VS Code extension - Jeremy Sylvestre, jsylvest at ualberta.ca
  • Re: [isabelle] VS Code extension - Jeremy Sylvestre, jsylvest at ualberta.ca
• Wed, 03 Mar 2021
  • Re: [isabelle] Fixing type variables in locales - Makarius, makarius at sketis.net
  • Re: [isabelle] Fixing type variables in locales - Wolfgang Jeltsch, wolfgang-it at jeltsch.info
  • [isabelle] SPIN 2021 - Deadline extension to April 20 - Laarman, A.W., a.w.laarman at liacs.leidenuniv.nl
  • [isabelle] building the document in Windows from Isabelle/jEdit - Stepan Holub, holub at karlin.mff.cuni.cz
  • [isabelle] Towards a formalization of elements of the foundations of category theory in ZFC in HOL - Mikhail Chekhov, mikhail.chekhov.w at gmail.com
• Thu, 04 Mar 2021
  • [isabelle] Isabelle 2021 Word Library - Freek Verbeek, freek at vt.edu
  • [isabelle] ATVA 2021 - Second Call for Papers - Giles Reger, giles.reger at manchester.ac.uk
  • Re: [isabelle] Python client to Isabelle server - Makarius, makarius at sketis.net
• Fri, 05 Mar 2021
  • Re: [isabelle] Isabelle 2021 Word Library - Peter Lammich, lammich at in.tum.de
  • Re: [isabelle] Isabelle 2021 Word Library - Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de
  • [isabelle] New in the AFP: Mereology - Tobias Nipkow, nipkow at in.tum.de
  • [isabelle] Bitblasting via SAT and Argo - Thomas Sewell, tals4 at cam.ac.uk
  • [isabelle] by fact and try0 - Stepan Holub, holub at karlin.mff.cuni.cz
• Sat, 06 Mar 2021
  • [isabelle] Troubles building Pure; can't find Foreign.buildCall3 - Jakub Kądziołka, kuba at kadziolka.net
  • Re: [isabelle] Nitpick finds counterexample to proven lemma - Stepan Holub, holub at karlin.mff.cuni.cz
  • Re: [isabelle] Troubles building Pure; can't find Foreign.buildCall3 - Jakub Kądziołka, kuba at kadziolka.net
• Sun, 07 Mar 2021
  • [isabelle] Structure of Proofs - Jens-D. Doll, jens.doll at live.de
  • Re: [isabelle] Structure of Proofs - Dr A. Koutsoukou-Argyraki, ak2110 at cam.ac.uk
• Mon, 08 Mar 2021
  • Re: [isabelle] Remaining uses of "isabelle process" and "isabelle console" - Dominique Unruh, unruh at ut.ee
  • Re: [isabelle] Remaining uses of "isabelle process" and "isabelle console" - Makarius, makarius at sketis.net
  • Re: [isabelle] Remaining uses of "isabelle process" and "isabelle console" - Makarius, makarius at sketis.net
  • [isabelle] keywords "spark_open" :: thy_load (spark_siv) - Walther Neuper, walther.neuper at jku.at
  • Re: [isabelle] Structure of Proofs - Jens-D. Doll, jens.doll at live.de
  • Re: [isabelle] keywords "spark_open" :: thy_load (spark_siv) - Makarius, makarius at sketis.net
• Tue, 09 Mar 2021
  • [isabelle] 7th International Workshop on Proof eXchange for Theorem Proving (PxTP) - First CFP - Chantal Keller, chantal.keller at wanadoo.fr
  • [isabelle] New in the AFP: Quantum projective measurements - Lawrence Paulson, lp15 at cam.ac.uk
  • Re: [isabelle] by fact and try0 - Jasmin Blanchette via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk
• Wed, 10 Mar 2021
  • Re: [isabelle] keywords "spark_open" :: thy_load (spark_siv) - Walther Neuper, walther.neuper at jku.at
  • Re: [isabelle] keywords "spark_open" :: thy_load (spark_siv) - Makarius, makarius at sketis.net
• Thu, 11 Mar 2021
  • [isabelle] ML questions - Jaap Boender, jaapb at kerguelen.org
  • Re: [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 - Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de
  • [isabelle] Request for feedback: dedicated session or AFP entry for material on combinatorics? - Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de
  • Re: [isabelle] Request for feedback: dedicated session or AFP entry for material on combinatorics? - Lawrence Paulson, lp15 at cam.ac.uk
  • Re: [isabelle] Request for feedback: dedicated session or AFP entry for material on combinatorics? - Manuel Eberl, eberlm at in.tum.de
  • [isabelle] Well-behaved MacOS application for Isabelle 2021 - Frédéric Boulanger, frederic.boulanger at lri.fr
  • Re: [isabelle] Request for feedback: dedicated session or AFP entry for material on combinatorics? - Tobias Nipkow, nipkow at in.tum.de
• Fri, 12 Mar 2021
  • [isabelle] New in the AFP: The Hermite–Lindemann–Weierstraß Transcendence Theorem - Lawrence Paulson, lp15 at cam.ac.uk
  • Re: [isabelle] keywords "spark_open" :: thy_load (spark_siv) - Walther Neuper, walther.neuper at jku.at
  • Re: [isabelle] keywords "spark_open" :: thy_load (spark_siv) - Makarius, makarius at sketis.net
• Sat, 13 Mar 2021
  • [isabelle] Research Programmer in HoTT and Cubical Type Theory - Favonia via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk
  • [isabelle] Lecturer in Verification position at University of Sheffield: deadline 29 March 2021 - Andrei Popescu, andrei.h.popescu at gmail.com
  • Re: [isabelle] Request for feedback: dedicated session or AFP entry for material on combinatorics? - Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de
  • Re: [isabelle] ML questions - Thomas Sewell, tals4 at cam.ac.uk
  • Re: [isabelle] ML questions - Peter Lammich, lammich at in.tum.de
  • Re: [isabelle] Request for feedback: dedicated session or AFP entry for material on combinatorics? - Tobias Nipkow, nipkow at in.tum.de
• Sun, 14 Mar 2021
  • [isabelle] New in the AFP: Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation - Andreas Lochbihler, mail at andreas-lochbihler.de
  • [isabelle] Entire theory in JSON forma using scala-isabelle? - Alex Meyer, alex153 at outlook.lv
  • [isabelle] Pārs.: Entire theory in JSON forma using scala-isabelle? - Alex Meyer, alex153 at outlook.lv
• Mon, 15 Mar 2021
  • [isabelle] [CFP] Logical Frameworks and Meta-Languages: Theory and Practice - Enrico Tassi, Enrico.Tassi at inria.fr
  • Re: [isabelle] Entire theory in JSON forma using scala-isabelle? - Dominique Unruh, unruh at ut.ee
  • Re: [isabelle] Entire theory in JSON forma using scala-isabelle? - Makarius, makarius at sketis.net
  • [isabelle] A lemma about remove1 - Jakub Kądziołka, kuba at kadziolka.net
  • Re: [isabelle] A lemma about remove1 - Peter Lammich, lammich at in.tum.de
  • Re: [isabelle] building the document in Windows from Isabelle/jEdit - Makarius, makarius at sketis.net
  • [isabelle] Specifying a Universal Property in a locale definition - AARON CRIGHTON, crightoa at mcmaster.ca
• Tue, 16 Mar 2021
  • Re: [isabelle] A lemma about remove1 - Tobias Nipkow, nipkow at in.tum.de
  • [isabelle] 14th Conference on Intelligent Computer Mathematics (CICM 2021) Final call for papers, Conference Date: July 26-31, 2021 - Serge Autexier, serge.autexier at dfki.de
• Wed, 17 Mar 2021
  • [isabelle] 21st Midlands Graduate School in the Foundations of Computing Science: Final Call for Participation - Andrei Popescu, andrei.h.popescu at gmail.com
  • Re: [isabelle] Remaining uses of "isabelle process" and "isabelle console" - Dominique Unruh, unruh at ut.ee
  • Re: [isabelle] Remaining uses of "isabelle process" and "isabelle console" - Makarius, makarius at sketis.net
  • Re: [isabelle] Remaining uses of "isabelle process" and "isabelle console" - Makarius, makarius at sketis.net
• Thu, 18 Mar 2021
  • [isabelle] New in the AFP: Constructive Cryptography in HOL: the Communication Modeling Aspect - Thiemann, René, Rene.Thiemann at uibk.ac.at
  • [isabelle] \isakeyword in bold? - Tobias Nipkow, nipkow at in.tum.de
• Sat, 20 Mar 2021
  • [isabelle] Formal algorithms in Isabelle - is it OK to specify algorithm as definition or is specification as function required? - Alex Meyer, alex153 at outlook.lv
  • Re: [isabelle] Formal algorithms in Isabelle - is it OK to specify algorithm as definition or is specification as function required? - Jakub Kądziołka, kuba at kadziolka.net
• Sun, 21 Mar 2021
  • [isabelle] C-to-Isabelle multiple external files - Adriana Stancu, adriana.stancu95 at gmail.com
  • [isabelle] Weak lemma: sum_mset_diff - Jakub Kądziołka, kuba at kadziolka.net
• Mon, 22 Mar 2021
  • Re: [isabelle] Specifying a Universal Property in a locale definition - Mikhail Chekhov, mikhail.chekhov.w at gmail.com
  • [isabelle] Call for Papers: HotSpot 2021 - Toby Murray, toby.murray at unimelb.edu.au
  • Re: [isabelle] C-to-Isabelle multiple external files - Thomas Sewell, tals4 at cam.ac.uk
  • Re: [isabelle] C-to-Isabelle multiple external files - Yakoub Nemouchi, y.nemouchi at gmail.com
  • [isabelle] How to see the names of all active Isabelle sessions and how to export specific session? - Alex Meyer, alex153 at outlook.lv
  • Re: [isabelle] How to see the names of all active Isabelle sessions and how to export specific session? - Jakub Kądziołka, kuba at kadziolka.net
• Tue, 23 Mar 2021
  • Re: [isabelle] C-to-Isabelle multiple external files - Jaap Boender, jaapb at kerguelen.org
  • Re: [isabelle] Specifying a Universal Property in a locale definition - Mikhail Chekhov, mikhail.chekhov.w at gmail.com
• Wed, 24 Mar 2021
  • [isabelle] Possible problem with floating-point addition in Approximation etc. - Manuel Eberl, eberlm at in.tum.de
  • Re: [isabelle] Possible problem with floating-point addition in Approximation etc. - Manuel Eberl, eberlm at in.tum.de
  • [isabelle] hd and last of Nil - Stepan Holub, holub at karlin.mff.cuni.cz
  • Re: [isabelle] hd and last of Nil - Lawrence Paulson, lp15 at cam.ac.uk
  • Re: [isabelle] hd and last of Nil - Manuel Eberl, eberlm at in.tum.de
• Thu, 25 Mar 2021
  • Re: [isabelle] hd and last of Nil - Stepan Holub, holub at karlin.mff.cuni.cz
  • [isabelle] Evaluation of definitions defined inside a locale - Sanan Baena David Miguel (Dr), sanan at ntu.edu.sg
  • Re: [isabelle] hd and last of Nil - Tjark Weber, tjark.weber at it.uu.se
  • Re: [isabelle] hd and last of Nil - Manuel Eberl, eberlm at in.tum.de
  • [isabelle] CFP ICTCS 2021 - 22th Italian Conference on Theoretical Computer Science - Claudio Sacerdoti Coen, claudio.sacerdoticoen at unibo.it
  • Re: [isabelle] hd and last of Nil - Jeremy Dawson, Jeremy.Dawson at anu.edu.au
  • Re: [isabelle] hd and last of Nil - John F. Hughes, jfh at cs.brown.edu
  • Re: [isabelle] hd and last of Nil - Mario Carneiro, di.gama at gmail.com
  • Re: [isabelle] hd and last of Nil - Norrish, Michael (Data61, Acton), Michael.Norrish at data61.csiro.au
• Fri, 26 Mar 2021
  • Re: [isabelle] hd and last of Nil - Tjark Weber, tjark.weber at it.uu.se
  • Re: [isabelle] hd and last of Nil - Thomas Sewell, tals4 at cam.ac.uk
  • Re: [isabelle] hd and last of Nil - Kevin Kappelmann, kevin.kappelmann at tum.de
  • Re: [isabelle] Possible problem with floating-point addition in Approximation etc. - Fabian Immler via Cl-isabelle-users, cl-isabelle-users at lists.cam.ac.uk
  • Re: [isabelle] hd and last of Nil - Stepan Holub, holub at karlin.mff.cuni.cz
• Sat, 27 Mar 2021
  • [isabelle] Atb.: How to see the names of all active Isabelle sessions and how to export specific session? - Alex Meyer, alex153 at outlook.lv
  • [isabelle] Pārs.: How to see the names of all active Isabelle sessions and how to export specific session? - Alex Meyer, alex153 at outlook.lv
• Sun, 28 Mar 2021
  • [isabelle] I completed mmt_import but now I have some questions - Alex Meyer, alex153 at outlook.lv
  • [isabelle] Concerning Fun.swap - Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de
  • Re: [isabelle] I completed mmt_import but now I have some questions - Makarius, makarius at sketis.net
  • Re: [isabelle] Concerning Fun.swap - Lawrence Paulson, lp15 at cam.ac.uk
  • Re: [isabelle] Evaluation of definitions defined inside a locale - Thiemann, René, Rene.Thiemann at uibk.ac.at
  • [isabelle] Morello: Edinburgh research posts on capability-based security technologies - Ian Stark, Ian.Stark at ed.ac.uk
• Mon, 29 Mar 2021
  • [isabelle] Proof Ground 2021 - Call for Problems - Maximilian Haslbeck, haslbema at in.tum.de
  • Re: [isabelle] hd and last of Nil - Thomas Sewell, tals4 at cam.ac.uk
  • [isabelle] 2nd CfP: SCSS 2021 - Temur Kutsia, kutsia at risc.jku.at
  • [isabelle] Deadline Extension: April 5th, 20201, 14th Conference on Intelligent Computer Mathematics (CICM 2021) - Serge Autexier, serge.autexier at dfki.de
• Wed, 31 Mar 2021
  • Re: [isabelle] Evaluation of definitions defined inside a locale - Sanan Baena David Miguel (Dr), sanan at ntu.edu.sg
  • Re: [isabelle] Evaluation of definitions defined inside a locale - YAMADA, Akihisa, ayamada at trs.cm.is.nagoya-u.ac.jp
  • Re: [isabelle] Evaluation of definitions defined inside a locale - Sanan Baena David Miguel (Dr), sanan at ntu.edu.sg