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