Cl-isabelle-users January 2021 Archives by thread

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

• Re: [isabelle] Isabelle2021-RC0: Java/VM monitor , Makarius - Fri, 01 Jan 2021 09:38:35 +0000
  • Re: [isabelle] Isabelle2021-RC0: Java/VM monitor , Eugene W. Stark - Sun, 03 Jan 2021 16:35:04 +0000
    • Re: [isabelle] Isabelle2021-RC0: Java/VM monitor , Makarius - Sun, 10 Jan 2021 15:56:20 +0000
      • Re: [isabelle] Isabelle2021-RC0: Java/VM monitor , Eugene W. Stark - Sun, 10 Jan 2021 19:24:55 +0000
• Re: [isabelle] Several questions about the availability of certain specific proof tools for classical reasoning/simplification in Isabelle/HOL , Lawrence Paulson - Fri, 01 Jan 2021 16:29:06 +0000
  • Re: [isabelle] Several questions about the availability of certain specific proof tools for classical reasoning/simplification in Isabelle/HOL , Mikhail Chekhov - Fri, 01 Jan 2021 19:55:24 +0000
    • Re: [isabelle] Several questions about the availability of certain specific proof tools for classical reasoning/simplification in Isabelle/HOL , Mikhail Chekhov - Fri, 01 Jan 2021 21:45:02 +0000
      • Re: [isabelle] Several questions about the availability of certain specific proof tools for classical reasoning/simplification in Isabelle/HOL , Lawrence Paulson - Sat, 02 Jan 2021 11:14:28 +0000
• [isabelle] Cannot load theory when building , Kawin Worrasangasilpa - Sat, 02 Jan 2021 08:23:26 +0000
  • Re: [isabelle] Cannot load theory when building , Makarius - Sat, 02 Jan 2021 10:03:54 +0000
• Re: [isabelle] quote in mixfix annotation , Makarius - Sat, 02 Jan 2021 10:11:37 +0000
• Re: [isabelle] Issue with Isabelle/jEdit in fullscreen mode in macOS Big Sur , Makarius - Sat, 02 Jan 2021 10:25:42 +0000
  • Re: [isabelle] Issue with Isabelle/jEdit in fullscreen mode in macOS Big Sur , Makarius - Sun, 10 Jan 2021 16:09:40 +0000
• Re: [isabelle] Question about "try" and future tasks , Makarius - Sat, 02 Jan 2021 10:36:09 +0000
• Re: [isabelle] Bug report Isabelle 2019 and Isabelle 2020 , Makarius - Sat, 02 Jan 2021 10:40:04 +0000
• Re: [isabelle] Using LaTeX output print mode for source text , Makarius - Sat, 02 Jan 2021 10:48:08 +0000
• [isabelle] Bootstrap problem in Isabelle2021-RC1: Consumer thread failure: "Isabelle.Session.manager" , Florian Haftmann - Sun, 03 Jan 2021 09:44:58 +0000
  • Re: [isabelle] Bootstrap problem in Isabelle2021-RC1: Consumer thread failure: "Isabelle.Session.manager" , Makarius - Sun, 03 Jan 2021 11:27:14 +0000
• Re: [isabelle] Apple switching to ARM , Makarius - Sun, 03 Jan 2021 11:37:39 +0000
• Re: [isabelle] Any fans of "try"? , Makarius - Sun, 03 Jan 2021 11:53:25 +0000
• Re: [isabelle] sledgehammer (or Z3) internal error , Makarius - Sun, 03 Jan 2021 12:00:20 +0000
• Re: [isabelle] Custom fonts in browser_info html? , Makarius - Sun, 03 Jan 2021 12:03:16 +0000
  • Re: [isabelle] Custom fonts in browser_info html? , Dr. Brendan Patrick Mahony - Fri, 08 Jan 2021 04:09:48 +0000
    • Re: [isabelle] Custom fonts in browser_info html? , Makarius - Fri, 08 Jan 2021 15:29:36 +0000
• Re: [isabelle] Sledgehammer errors (Isabelle 2020) , Makarius - Sun, 03 Jan 2021 14:42:58 +0000
  • Re: [isabelle] Sledgehammer errors (Isabelle 2020) , Mathias Fleury - Sun, 03 Jan 2021 17:18:53 +0000
• [isabelle] CfP Theorem Proving Components for Educational Software at CADE-28 , Walther Neuper - Sun, 03 Jan 2021 16:33:48 +0000
• [isabelle] Go-to-definition doesn't work when exploring library. , Jakub Kądziołka - Sun, 03 Jan 2021 23:58:18 +0000
  • Re: [isabelle] Go-to-definition doesn't work when exploring library. , Makarius - Mon, 04 Jan 2021 12:37:38 +0000
• [isabelle] low-level code formalisations in Isabelle , Buday Gergely via Cl-isabelle-users - Mon, 04 Jan 2021 08:46:00 +0000
• [isabelle] FSCD 2021: Second Call for Papers , Carsten Fuhs - Mon, 04 Jan 2021 17:08:24 +0000
• [isabelle] Fwd: Re: Several questions about the availability of certain specific proof tools for classical reasoning/simplification in Isabelle/HOL , Thomas Sewell - Mon, 04 Jan 2021 17:23:13 +0000
• [isabelle] Research assistant/associate position at Imperial College London , Lorenzo Gheri - Mon, 04 Jan 2021 17:53:54 +0000
• [isabelle] Questionnaire on deployed verified systems , Alexander Kogtenkov via Cl-isabelle-users - Tue, 05 Jan 2021 12:24:13 +0000
• [isabelle] Questions about "transfer" , Manuel Eberl - Tue, 05 Jan 2021 12:40:37 +0000
  • Re: [isabelle] Questions about "transfer" , Andreas Lochbihler - Wed, 06 Jan 2021 20:46:05 +0000
  • <Possible follow-ups>
  • Re: [isabelle] Questions about "transfer" , Mikhail Chekhov - Tue, 05 Jan 2021 23:20:18 +0000
    • Re: [isabelle] Questions about "transfer" , Mikhail Chekhov - Wed, 06 Jan 2021 23:30:49 +0000
• [isabelle] ITP2021: Second Call for Workshops (Deadline 11 January 2021) , itp2021-workshops - Tue, 05 Jan 2021 15:05:54 +0000
• [isabelle] Isabelle2021-RC1 - Any way to limit "veriT" memory use? , Eugene W. Stark - Tue, 05 Jan 2021 23:28:42 +0000
  • Re: [isabelle] Isabelle2021-RC1 - Any way to limit "veriT" memory use? , Mathias Fleury - Wed, 06 Jan 2021 08:29:51 +0000
    • Re: [isabelle] Isabelle2021-RC1 - Any way to limit "veriT" memory use? , Eugene W. Stark - Wed, 06 Jan 2021 11:03:38 +0000
      • Re: [isabelle] Isabelle2021-RC1 - Any way to limit "veriT" memory use? , Eugene W. Stark - Sun, 10 Jan 2021 20:56:25 +0000
      • Re: [isabelle] Isabelle2021-RC1 - Any way to limit "veriT" memory use? , Mathias Fleury - Mon, 11 Jan 2021 07:28:36 +0000
      • Re: [isabelle] Isabelle2021-RC1 - Any way to limit "veriT" memory use? , Eugene W. Stark - Mon, 11 Jan 2021 13:52:46 +0000
      • Re: [isabelle] Isabelle2021-RC1 - Any way to limit "veriT" memory use? , Mathias Fleury - Thu, 14 Jan 2021 06:23:58 +0000
      • Re: [isabelle] Isabelle2021-RC1 - Any way to limit "veriT" memory use? , Thomas Sewell - Thu, 14 Jan 2021 16:27:58 +0000
• [isabelle] Call for Papers: Tests and Proofs 2021 (TAP 2021) , Frederic Loulergue - Wed, 06 Jan 2021 09:29:09 +0000
• [isabelle] Isabelle2021-RC1 - editing below sometimes causes rechecking above? , Eugene W. Stark - Wed, 06 Jan 2021 14:34:26 +0000
  • Re: [isabelle] Isabelle2021-RC1 - editing below sometimes causes rechecking above? , Makarius - Sun, 10 Jan 2021 15:57:34 +0000
  • <Possible follow-ups>
  • Re: [isabelle] Isabelle2021-RC1 - editing below sometimes causes rechecking above? , Fabian Immler via Cl-isabelle-users - Fri, 08 Jan 2021 15:53:10 +0000
    • Re: [isabelle] Isabelle2021-RC1 - editing below sometimes causes rechecking above? , Makarius - Sun, 10 Jan 2021 15:58:33 +0000
• [isabelle] Isabelle2021-RC1 - error highlighting , Mathias Fleury - Wed, 06 Jan 2021 14:42:55 +0000
  • Re: [isabelle] Isabelle2021-RC1 - error highlighting , Makarius - Thu, 07 Jan 2021 13:57:52 +0000
    • Re: [isabelle] Isabelle2021-RC1 - error highlighting , Mathias Fleury - Thu, 07 Jan 2021 15:40:29 +0000
      • Re: [isabelle] Isabelle2021-RC1 - error highlighting , Makarius - Fri, 08 Jan 2021 20:17:48 +0000
• [isabelle] fully funded PhD position on verification of industrial robots at University of Sheffield -- application deadline coming soon (Jan. 13) , Andrei Popescu - Wed, 06 Jan 2021 17:12:26 +0000
• [isabelle] [TFP'21] final call for papers: Trends in Functional Programming 2021, 17-19 February (online event with Lambda Days 2021 & TFPIE 2021) , Peter Achten - Fri, 08 Jan 2021 08:09:47 +0000
• [isabelle] Variable both free and bound?! , Jakub Kądziołka - Fri, 08 Jan 2021 22:34:26 +0000
  • Re: [isabelle] Variable both free and bound?! , Buday Gergely István via Cl-isabelle-users - Sun, 10 Jan 2021 16:37:43 +0000
    • Re: [isabelle] Variable both free and bound?! , Jakub Kądziołka - Sun, 10 Jan 2021 16:39:41 +0000
    • Re: [isabelle] Variable both free and bound?! , Makarius - Sun, 10 Jan 2021 18:34:36 +0000
  • Re: [isabelle] Variable both free and bound?! , Makarius - Sun, 10 Jan 2021 18:20:58 +0000
• [isabelle] Isabelle2021-RC1 - sledgehammer suggestion "by presburger" sometimes fails , Eugene W. Stark - Sat, 09 Jan 2021 15:21:35 +0000
• [isabelle] Strange "Tactic failed" error in lift_definition with (code_dt) seemingly depending on syntactic details , Florian Märkl - Sat, 09 Jan 2021 18:12:28 +0000
• [isabelle] Detecting undefined , David Kretzmer - Sat, 09 Jan 2021 19:31:56 +0000
  • Re: [isabelle] Detecting undefined , Tobias Nipkow - Mon, 11 Jan 2021 11:35:22 +0000
    • Re: [isabelle] Detecting undefined , Manuel Eberl - Mon, 11 Jan 2021 11:47:44 +0000
      • Re: [isabelle] Detecting undefined , David Kretzmer - Mon, 11 Jan 2021 14:14:13 +0000
      • Re: [isabelle] Detecting undefined , Lawrence Paulson - Mon, 11 Jan 2021 14:21:35 +0000
      • Re: [isabelle] Detecting undefined , David Kretzmer - Mon, 11 Jan 2021 17:48:02 +0000
• [isabelle] brute force search in lists , Stepan Holub - Sun, 10 Jan 2021 11:16:33 +0000
  • Re: [isabelle] brute force search in lists , Manuel Eberl - Mon, 11 Jan 2021 08:11:18 +0000
• [isabelle] Isabelle 2021-RC1: Problem with fonts in jEdit , Thiemann, René - Sun, 10 Jan 2021 13:29:29 +0000
  • Re: [isabelle] Isabelle 2021-RC1: Problem with fonts in jEdit , Makarius - Sun, 10 Jan 2021 16:04:50 +0000
    • Re: [isabelle] Isabelle 2021-RC1: Problem with fonts in jEdit , Thiemann, René - Mon, 11 Jan 2021 17:53:18 +0000
• [isabelle] Isabelle2021-RC2 available for testing , Makarius - Sun, 10 Jan 2021 15:52:52 +0000
  • Re: [isabelle] Isabelle2021-RC2: improved HTML presentation , Makarius - Sun, 10 Jan 2021 18:47:47 +0000
    • Re: [isabelle] Isabelle2021-RC2: improved HTML presentation , Jakub Kądziołka - Sun, 10 Jan 2021 22:12:41 +0000
      • Re: [isabelle] Isabelle2021-RC2: improved HTML presentation , Makarius - Mon, 11 Jan 2021 15:18:25 +0000
      • Re: [isabelle] Isabelle2021-RC2: improved HTML presentation , Makarius - Mon, 11 Jan 2021 15:26:08 +0000
    • Re: [isabelle] Isabelle2021-RC2: improved HTML presentation , Pedro Sánchez Terraf - Mon, 18 Jan 2021 16:14:19 +0000
• [isabelle] F-IDE 2021 - 2nd Call for Papers , Makarius - Sun, 10 Jan 2021 18:24:09 +0000
• Re: [isabelle] Debug facilities of locales , Makarius - Sun, 10 Jan 2021 18:26:59 +0000
• [isabelle] Updating AFP entry , Pedro Sánchez Terraf - Mon, 11 Jan 2021 18:14:39 +0000
  • Re: [isabelle] Updating AFP entry , Tobias Nipkow - Tue, 12 Jan 2021 07:36:17 +0000
    • Re: [isabelle] Updating AFP entry , Gerwin Klein - Tue, 12 Jan 2021 23:26:59 +0000
• [isabelle] New in the AFP: The HOL-CSP Refinement Toolkit , Manuel Eberl - Tue, 12 Jan 2021 12:10:00 +0000
• [isabelle] Isabelle2021-RC2: slight regression in HTML output , Jakub Kądziołka - Tue, 12 Jan 2021 23:34:28 +0000
• [isabelle] AFP 2021 preparations , Gerwin Klein - Tue, 12 Jan 2021 23:39:29 +0000
  • Re: [isabelle] AFP 2021 preparations , Gerwin Klein - Fri, 15 Jan 2021 10:24:24 +0000
• [isabelle] New AFP entry: JinjaDCI: a Java semantics with dynamic class initialization , Tobias Nipkow - Wed, 13 Jan 2021 09:36:41 +0000
• [isabelle] SMT 2021 Workshop: Call for Papers , Nadel, Alexander - Wed, 13 Jan 2021 12:25:47 +0000
• [isabelle] Some lemmas on factorial rings , Jakub Kądziołka - Wed, 13 Jan 2021 23:20:44 +0000
  • Re: [isabelle] Some lemmas on factorial rings , Florian Haftmann - Thu, 14 Jan 2021 15:28:14 +0000
• Re: [isabelle] Lemma suggestion to Function_Algebras , Florian Haftmann - Thu, 14 Jan 2021 15:20:51 +0000
• [isabelle] [CFP] Logical Frameworks and Meta-Languages: Theory and Practice , Enrico Tassi - Fri, 15 Jan 2021 16:30:20 +0000
• [isabelle] Two questions about the availability of certain functionality from the public interface associated with the Isabelle/ML infrastructure , Mikhail Chekhov - Fri, 15 Jan 2021 21:46:47 +0000
  • Re: [isabelle] Two questions about the availability of certain functionality from the public interface associated with the Isabelle/ML infrastructure , Florian Haftmann - Sat, 16 Jan 2021 09:21:07 +0000
  • <Possible follow-ups>
  • Re: [isabelle] Two questions about the availability of certain functionality from the public interface associated with the Isabelle/ML infrastructure , Mikhail Chekhov - Sat, 16 Jan 2021 14:15:22 +0000
• [isabelle] Isabelle keywords , Stephan Merz - Sat, 16 Jan 2021 09:55:52 +0000
  • Re: [isabelle] Isabelle keywords , Makarius - Sat, 16 Jan 2021 13:03:13 +0000
• [isabelle] Fwd: ITP 2021: Third Call for Papers , Cezary Kaliszyk - Sat, 16 Jan 2021 16:10:27 +0000
• [isabelle] Epigenetics and similar Phenomena , Jens-D. Doll - Sun, 17 Jan 2021 11:57:21 +0000
• [isabelle] Derive bounded sets from extended nat , Kruse, Kevin - Sun, 17 Jan 2021 15:20:18 +0000
  • Re: [isabelle] Derive bounded sets from extended nat , Manuel Eberl - Mon, 18 Jan 2021 10:25:08 +0000
  • <Possible follow-ups>
  • Re: [isabelle] Derive bounded sets from extended nat , Kevin Kruse - Mon, 18 Jan 2021 22:06:11 +0000
• [isabelle] Some lemmas with a combinatoric flavor , Jakub Kądziołka - Sun, 17 Jan 2021 23:22:49 +0000