Cl-isabelle-users October 2020 Archives by subject

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

• [isabelle] Benchmark suite for Isabelle's `rewrite` tactic
  • Zack Grannan, zachary.grannan at imdea.org - Thu, 15 Oct 2020 12:56:39 +0100
  • Makarius, makarius at sketis.net - Mon, 19 Oct 2020 16:48:55 +0100
• [isabelle] CADE-28: Call for Papers, Workshops, Tutorials and Competitions
  • Sophie Tourret, stourret at mpi-inf.mpg.de - Wed, 21 Oct 2020 12:32:16 +0100
• [isabelle] CfP: AMAI Special Issue on Theoretical and Practical Aspects of Unification
  • Temur Kutsia, kutsia at risc.jku.at - Wed, 07 Oct 2020 12:17:09 +0100
• [isabelle] clashes in _graph names generated by mutual recursion
  • Fernandez, Matthew, matthew.fernandez at intel.com - Thu, 15 Oct 2020 22:17:14 +0100
• [isabelle] Degree of an almost everywhere constant function
  • Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de - Thu, 15 Oct 2020 15:41:50 +0100
  • Manuel Eberl, eberlm at in.tum.de - Thu, 15 Oct 2020 15:47:04 +0100
• [isabelle] Duplicate algebra tactic
  • Jakub Kądziołka, kuba at kadziolka.net - Wed, 07 Oct 2020 15:12:45 +0100
• [isabelle] Error in Eisbach syntax diagram
  • Wolfgang Jeltsch, wolfgang-it at jeltsch.info - Tue, 06 Oct 2020 22:26:59 +0100
  • Klein, Gerwin (Data61, Kensington NSW), Gerwin.Klein at data61.csiro.au - Mon, 19 Oct 2020 01:56:41 +0100
• [isabelle] Faculty position at Portland State University
  • Andrew Tolmach, tolmach at pdx.edu - Sun, 25 Oct 2020 21:02:12 +0000
• [isabelle] F-IDE 2021 - Call for Papers
  • Andrei Paskevich, andrei.paskevich at lri.fr - Mon, 19 Oct 2020 17:17:44 +0100
• [isabelle] finite order allows maxima
  • Stepan Holub, holub at karlin.mff.cuni.cz - Sat, 03 Oct 2020 09:38:03 +0100
  • Dmitriy Traytel, traytel at di.ku.dk - Sun, 04 Oct 2020 13:31:54 +0100
  • Tobias Nipkow, nipkow at in.tum.de - Mon, 05 Oct 2020 17:23:12 +0100
  • Manuel Eberl, eberlm at in.tum.de - Mon, 05 Oct 2020 17:30:29 +0100
  • Tobias Nipkow, nipkow at in.tum.de - Tue, 06 Oct 2020 08:03:24 +0100
  • Bisping, Benjamin, benjamin.bisping at tu-berlin.de - Tue, 06 Oct 2020 10:27:17 +0100
  • Lawrence Paulson, lp15 at cam.ac.uk - Tue, 06 Oct 2020 10:38:22 +0100
  • Stepan Holub, holub at karlin.mff.cuni.cz - Tue, 06 Oct 2020 10:53:30 +0100
  • Florian Haftmann, florian.haftmann at informatik.tu-muenchen.de - Tue, 06 Oct 2020 10:59:04 +0100
  • Manuel Eberl, eberlm at in.tum.de - Tue, 06 Oct 2020 11:57:22 +0100
  • Tobias Nipkow, nipkow at in.tum.de - Tue, 06 Oct 2020 20:47:10 +0100
  • Jakub Kądziołka, kuba at kadziolka.net - Wed, 07 Oct 2020 20:50:20 +0100
• [isabelle] FSCD 2021: Call for Workshop Proposals
  • Carsten Fuhs, carsten at dcs.bbk.ac.uk - Wed, 28 Oct 2020 11:34:49 +0000
• [isabelle] How do I set --maxheap greater than 16G on Linux?
  • Eugene W. Stark, isabelle-users at starkeffect.com - Sat, 10 Oct 2020 02:12:23 +0100
  • Eugene W. Stark, isabelle-users at starkeffect.com - Sat, 10 Oct 2020 17:57:31 +0100
• [isabelle] How to make Eisbach's match functionality available from Isabelle/ML?
  • Mikhail Chekhov, mikhail.chekhov.w at gmail.com - Sun, 04 Oct 2020 18:47:42 +0100
• Re: [isabelle] How to make Eisbach's match functionality available from Isabelle/ML?
  • Mikhail Chekhov, mikhail.chekhov.w at gmail.com - Mon, 05 Oct 2020 23:42:20 +0100
• [isabelle] Improvement suggestion for isabelle process
  • Devant, Pascal, pascal.devant at rwth-aachen.de - Fri, 09 Oct 2020 23:43:12 +0100
• [isabelle] Lemma suggestion to Function_Algebras
  • Yamada, Akihisa, ayamada at trs.cm.is.nagoya-u.ac.jp - Mon, 05 Oct 2020 01:49:49 +0100
  • Yamada, Akihisa, ayamada at trs.cm.is.nagoya-u.ac.jp - Mon, 05 Oct 2020 02:04:42 +0100
• [isabelle] list_all vs set membership
  • Jakub Kądziołka, kuba at kadziolka.net - Wed, 14 Oct 2020 23:04:19 +0100
  • Andrei Popescu, andrei.h.popescu at gmail.com - Wed, 14 Oct 2020 23:31:55 +0100
  • Lawrence Paulson, lp15 at cam.ac.uk - Thu, 15 Oct 2020 08:58:51 +0100
  • Lukas Bulwahn, lukas.bulwahn at gmail.com - Thu, 15 Oct 2020 09:19:42 +0100
• [isabelle] make Isabelle accessible?
  • Walther Neuper, walther.neuper at jku.at - Mon, 19 Oct 2020 09:28:24 +0100
• [isabelle] Name clash in "let" definitions
  • Martin Desharnais, martin.desharnais at posteo.de - Thu, 29 Oct 2020 09:19:53 +0000
  • Mathias Fleury, mathias.fleury12 at gmail.com - Thu, 29 Oct 2020 09:49:41 +0000
  • Martin Desharnais, martin.desharnais at posteo.de - Thu, 29 Oct 2020 10:19:01 +0000
  • Peter Lammich, lammich at in.tum.de - Thu, 29 Oct 2020 11:01:57 +0000
• [isabelle] New in the AFP: A Sound Type System for Physical Quantities, Units, and Measurements
  • Thiemann, René, Rene.Thiemann at uibk.ac.at - Wed, 28 Oct 2020 11:29:17 +0000
• [isabelle] Performance problem with Simpl and Isabelle simplifier
  • Yulu Pan, pandaman at is.s.u-tokyo.ac.jp - Sat, 31 Oct 2020 15:02:51 +0000
• [isabelle] PhD and Postdoc positions at the University of Copenhagen
  • Dmitriy Traytel, traytel at di.ku.dk - Fri, 09 Oct 2020 21:13:09 +0100
• [isabelle] Questions on locales - structure keyword and local definitions
  • C.L. Edmonds, cle47 at cam.ac.uk - Tue, 06 Oct 2020 13:05:53 +0100
• [isabelle] quote in mixfix annotation
  • Walther Neuper, walther.neuper at jku.at - Tue, 06 Oct 2020 09:04:55 +0100
• [isabelle] Research position at fortiss, Munich
  • Chuangjie Xu, cj-xu at outlook.com - Mon, 26 Oct 2020 13:14:36 +0000
• [isabelle] Research position in Formal Verification (m/f/x) at HENSOLDT Cyber in Munich
  • Jaap Boender, jaapb at kerguelen.org - Tue, 20 Oct 2020 13:07:42 +0100
• [isabelle] scope of facts arising from `subgoal`
  • Peter Gammie, peteg42 at gmail.com - Mon, 12 Oct 2020 22:27:06 +0100
  • Andreas Lochbihler, mail at andreas-lochbihler.de - Tue, 13 Oct 2020 06:34:49 +0100
  • Peter Gammie, peteg42 at gmail.com - Sat, 17 Oct 2020 23:19:21 +0100
• [isabelle] Second Call for Presentations: PriSC 2021 @ POPL 2021
  • PriSC PC Chairs, prisc.pc.chairs at gmail.com - Tue, 27 Oct 2020 21:38:15 +0000
• [isabelle] Sledgehammer proof reconstruction failed
  • Jakub Kądziołka, kuba at kadziolka.net - Tue, 13 Oct 2020 19:34:09 +0100
  • Mathias Fleury, mathias.fleury12 at gmail.com - Sat, 31 Oct 2020 08:49:47 +0000
• [isabelle] Survey Paper
  • Tobias Nipkow, nipkow at in.tum.de - Mon, 19 Oct 2020 06:56:10 +0100
  • Qian Hong, fracting at gmail.com - Tue, 20 Oct 2020 01:02:22 +0100
  • Tobias Nipkow, nipkow at in.tum.de - Tue, 20 Oct 2020 13:33:30 +0100
  • Qian Hong, fracting at gmail.com - Tue, 20 Oct 2020 14:09:31 +0100
• [isabelle] Unnecessary assumption in HOL-Analysis.Convex.convex_on_alt
  • Jakub Kądziołka, kuba at kadziolka.net - Mon, 05 Oct 2020 14:02:59 +0100
• Re: [isabelle] Unnecessary assumption in HOL-Analysis.Convex.convex_on_alt
  • Lawrence Paulson, lp15 at cam.ac.uk - Tue, 06 Oct 2020 10:21:27 +0100
• [isabelle] Weak lemmas in HOL-Analysis.Affine
  • Jakub Kądziołka, kuba at kadziolka.net - Fri, 16 Oct 2020 15:16:49 +0100
  • Lawrence Paulson, lp15 at cam.ac.uk - Fri, 16 Oct 2020 15:30:36 +0100
  • Lawrence Paulson, lp15 at cam.ac.uk - Sat, 17 Oct 2020 11:22:22 +0100
  • Jakub Kądziołka, kuba at kadziolka.net - Sat, 17 Oct 2020 13:37:49 +0100
  • Lawrence Paulson, lp15 at cam.ac.uk - Sat, 17 Oct 2020 13:59:31 +0100
  • Jakub Kądziołka, kuba at kadziolka.net - Sat, 17 Oct 2020 14:29:33 +0100
• [isabelle] writing a proof method after "qed"
  • Lawrence Paulson, lp15 at cam.ac.uk - Wed, 28 Oct 2020 09:55:10 +0000
  • Jakub Kądziołka, kuba at kadziolka.net - Wed, 28 Oct 2020 10:04:49 +0000
  • Lawrence Paulson, lp15 at cam.ac.uk - Wed, 28 Oct 2020 10:51:58 +0000
  • Manuel Eberl, eberlm at in.tum.de - Wed, 28 Oct 2020 10:54:29 +0000