Stream: Mirror: Isabelle Users Mailing List

Topics:

• [isabelle] Teaching Isabelle/HOL foundations (7 messages, latest: Aug 15 2022 at 01:31)
• [isabelle] New in the AFP: Isabelle/Solidity: A Deep Embe... (1 message, latest: Aug 12 2022 at 18:29)
• [isabelle] Interpretation in locale context (4 messages, latest: Aug 12 2022 at 13:39)
• [isabelle] New in the AFP: Verified Complete Test Strateg... (1 message, latest: Aug 11 2022 at 15:39)
• [isabelle] Registration open: Sixteenth International Tbi... (1 message, latest: Aug 11 2022 at 02:14)
• [isabelle] Startup Error (7 messages, latest: Aug 10 2022 at 12:45)
• [isabelle] "ML Cleanup" issues on a Windows machine (3 messages, latest: Aug 09 2022 at 10:41)
• [isabelle] Infinite chains in sublocale interpretations (1 message, latest: Aug 09 2022 at 02:31)
• [isabelle] Isabelle2022-RC0 sneak preview (1 message, latest: Aug 08 2022 at 21:41)
• [isabelle] Hybrid Isabelle Workshop 2022: Thu 11-Aug-2022... (1 message, latest: Aug 08 2022 at 17:50)
• [isabelle] Reverse or backwards induction (4 messages, latest: Aug 08 2022 at 13:13)
• [isabelle] Does this function terminate (5 messages, latest: Aug 07 2022 at 09:52)
• [isabelle] Registration open: ICTAC autumn school, Septem... (3 messages, latest: Aug 07 2022 at 06:09)
• [isabelle] Remainder: ISR 2022 Registration Open (1 message, latest: Aug 07 2022 at 06:08)
• [isabelle] CICM 2022: Call for Participation (1 message, latest: Aug 07 2022 at 06:06)
• [isabelle] PhD student in Computing Science on the topic ... (1 message, latest: Aug 05 2022 at 13:07)
• [isabelle] Call for participation: EuroProofNet Workshop ... (1 message, latest: Aug 04 2022 at 05:58)
• [isabelle] Isabelle/ML problem using local_setup (1 message, latest: Aug 03 2022 at 12:50)
• [isabelle] Final CfP: FM 2023 - 25th International Sympos... (1 message, latest: Aug 01 2022 at 10:07)
• [isabelle] 13th International School on Rewriting (ISR 20... (2 messages, latest: Jul 31 2022 at 07:44)
• [isabelle] PhD and Postdoctoral positions in Formal Metho... (1 message, latest: Jul 31 2022 at 07:38)
• [isabelle] Codegen for List.member overwrites List struct... (4 messages, latest: Jul 28 2022 at 07:04)
• [isabelle] Call for Participation -- Mathematics of Progr... (1 message, latest: Jul 27 2022 at 08:52)
• [isabelle] datatype command not documented in isar-ref.pdf (1 message, latest: Jul 27 2022 at 08:45)
• [isabelle] Document prep. from a dedicated session (1 message, latest: Jul 27 2022 at 07:23)
• [isabelle] Frustrating case of simplifier looping (2 messages, latest: Jul 25 2022 at 14:46)
• [isabelle] [Patch] Unclear behaviour of HOL-Library.Code_... (1 message, latest: Jul 25 2022 at 08:21)
• [isabelle] Mac M1 12.4: nitpick and sledgehammer (14 messages, latest: Jul 24 2022 at 15:52)
• [isabelle] smt (verit): exception THM 0 raised (line 312 ... (2 messages, latest: Jul 21 2022 at 16:56)
• [isabelle] Registration Open: ISR 2022, September 19-24, ... (1 message, latest: Jul 21 2022 at 10:24)
• [isabelle] reviewer of paper using somewhat isabelle-insp... (6 messages, latest: Jul 20 2022 at 19:57)
• [isabelle] Request for Feedback - New Code Generator Targ... (1 message, latest: Jul 20 2022 at 19:14)
• [isabelle] abbreviations and eta contraction (2 messages, latest: Jul 20 2022 at 13:43)
• [isabelle] "~~/src/HOL/Tools/ATP/atp_problem.ML": unexpec... (2 messages, latest: Jul 19 2022 at 14:27)
• [isabelle] smt (z3): Replaying the proof trace produced b... (1 message, latest: Jul 19 2022 at 11:53)
• [isabelle] First Call for Papers - ABZ 2023: Internationa... (1 message, latest: Jul 17 2022 at 21:41)
• [isabelle] how to use auto2? (2 messages, latest: Jul 17 2022 at 13:19)
• [isabelle] Weak lemma: sum_mset_diff (2 messages, latest: Jul 15 2022 at 15:46)
• [isabelle] 2nd CFP - IFL22 - The 34th Symposium on Implem... (1 message, latest: Jul 15 2022 at 09:57)
• [isabelle] Registration Open: Computational Logic Autumn ... (1 message, latest: Jul 15 2022 at 05:44)
• [isabelle] Annoucement: Isabelle/C_2021-1 Release (1 message, latest: Jul 13 2022 at 15:00)
• [isabelle] New AFP website: past versions of entries are ... (4 messages, latest: Jul 13 2022 at 09:16)
• [isabelle] Call for talks/participation - EuroProofNet Wo... (1 message, latest: Jul 12 2022 at 13:34)
• [isabelle] RELEASE : Isabelle/DOF 1.3 (2021-1) (1 message, latest: Jul 12 2022 at 10:04)
• [isabelle] PhD Student or Postdoc Position in Alexander v... (1 message, latest: Jul 12 2022 at 10:04)
• [isabelle] Pending sort hypothesis with definition (4 messages, latest: Jul 12 2022 at 09:18)
• [isabelle] Equational reasoning with "undefined" expressions (2 messages, latest: Jul 12 2022 at 08:51)
• [isabelle] New in the AFP: a classic proof by Pólya (1 message, latest: Jul 11 2022 at 13:13)
• [isabelle] Is there a collection of basic counting proper... (14 messages, latest: Jul 11 2022 at 09:11)
• [isabelle] New in the AFP: A Reuse-Based Multi-Stage Comp... (1 message, latest: Jul 11 2022 at 05:27)
• [isabelle] Certified Symbolic-Numeric Computation (1 message, latest: Jul 07 2022 at 08:48)
• [isabelle] CICM 2022, final call for applications to the ... (2 messages, latest: Jul 06 2022 at 16:15)
• [isabelle] How to: Sublocales in Isabelle/ML (2 messages, latest: Jul 06 2022 at 11:55)
• [isabelle] Kodkod warning: cannot launch SAT solver, fall... (1 message, latest: Jul 06 2022 at 05:49)
• [isabelle] CFA International Symposium on ARC (1 message, latest: Jul 05 2022 at 20:19)
• [isabelle] New in the AFP: Boolos's Curious Inference (1 message, latest: Jul 04 2022 at 15:39)
• [isabelle] What causes the stucking? (1 message, latest: Jul 02 2022 at 14:21)
• [isabelle] AFP site: Congrats and question (1 message, latest: Jul 01 2022 at 12:16)
• [isabelle] Mac M1 12.4 (4 messages, latest: Jul 01 2022 at 08:00)
• [isabelle] Call for Papers: Unsound - Sources of Unsoundn... (1 message, latest: Jul 01 2022 at 08:00)
• [isabelle] New in the AFP: Real-Time Double-Ended Queue (1 message, latest: Jul 01 2022 at 07:06)
• [isabelle] Isabelle Workshop 2022 at FLoC (1 message, latest: Jun 30 2022 at 19:31)
• [isabelle] Proving subgoals with bound variables with ass... (1 message, latest: Jun 30 2022 at 12:10)
• [isabelle] CSL'23 - last call for papers (1 message, latest: Jun 29 2022 at 15:50)
• [isabelle] Refinement Framework (1 message, latest: Jun 29 2022 at 06:56)
• [isabelle] Poly/ML allocation limit (6 messages, latest: Jun 28 2022 at 19:24)
• [isabelle] Refinement Framework (1 message, latest: Jun 28 2022 at 17:07)
• [isabelle] Sledgehammer in Locale Context? (10 messages, latest: Jun 24 2022 at 17:54)
• [isabelle] Dependent Quotients for HOL (1 message, latest: Jun 24 2022 at 15:52)
• [isabelle] New in the AFP: IsaNet: Formalization of a Ver... (1 message, latest: Jun 24 2022 at 14:42)
• [isabelle] sublocale with definition (4 messages, latest: Jun 23 2022 at 19:39)
• [isabelle] design: New AFP Website (5 messages, latest: Jun 23 2022 at 09:22)
• [isabelle] ICTAC autumn school - registration open (1 message, latest: Jun 23 2022 at 08:56)
• [isabelle] How to print the axioms of the current theory (2 messages, latest: Jun 22 2022 at 22:28)
• [isabelle] ICTAC 2022 - Final CFP - Tbilisi, Georgia (1 message, latest: Jun 21 2022 at 10:46)
• [isabelle] [FSEN 2023] First Call for Papers FSEN 2023 (1 message, latest: Jun 20 2022 at 10:32)
• [isabelle] ISR 2022, September 19-24, 2022, Tbilisi, Geor... (1 message, latest: Jun 19 2022 at 08:46)
• [isabelle] Release of Dkcheck 2.7, a type-checker for Ded... (1 message, latest: Jun 18 2022 at 10:23)
• [isabelle] Premise extraction with the use of Isabelle/Scala (6 messages, latest: Jun 18 2022 at 09:11)
• [isabelle] 17th International Computer Science Symposium ... (1 message, latest: Jun 17 2022 at 18:15)
• [isabelle] Logic in Question / Couturat by Anne-Françoise... (1 message, latest: Jun 16 2022 at 08:57)
• [isabelle] New in the AFP: Finite Fields (1 message, latest: Jun 16 2022 at 07:14)
• [isabelle] Mistakes in and fixes to Isabelle proofs (9 messages, latest: Jun 15 2022 at 01:51)
• [isabelle] Certified Programs and Proofs (CPP) 2023 Call ... (1 message, latest: Jun 14 2022 at 20:14)
• [isabelle] CALL FOR PAPERS - IFL22 - The 34th Symposium o... (1 message, latest: Jun 14 2022 at 08:46)
• [isabelle] ICLP 2022: Call for Participation (1 message, latest: Jun 14 2022 at 08:46)
• [isabelle] Women in Logic 2022 - First Call for Participa... (1 message, latest: Jun 13 2022 at 16:30)
• [isabelle] Problem with lift_definition (code_dt) (1 message, latest: Jun 13 2022 at 15:03)
• [isabelle] A formal model of IEEE-754 floating-point arit... (17 messages, latest: Jun 09 2022 at 23:39)
• [isabelle] Isabelle parsers (8 messages, latest: Jun 08 2022 at 12:31)
• [isabelle] Implementing two ML functions regarding depend... (4 messages, latest: Jun 07 2022 at 15:37)
• [isabelle] New in the AFP: Diophantine Equations and the ... (1 message, latest: Jun 07 2022 at 11:40)
• [isabelle] EuroProofNet Call for Short-Term Scientific Mi... (1 message, latest: Jun 06 2022 at 11:52)
• [isabelle] New in the AFP: Reducing Rewrite Properties to... (1 message, latest: Jun 06 2022 at 07:00)
• [isabelle] Webpage for generating LaTeX snippets from Isa... (1 message, latest: Jun 02 2022 at 10:05)
• [isabelle] ML Family Workshop 2022: DEADLINE EXTENSION (1 message, latest: May 31 2022 at 16:12)
• [isabelle] Job offer / Researcher-Engineer / Inria, France (1 message, latest: May 31 2022 at 14:01)
• [isabelle] Deadline Extension: ICTAC 2022 (1 message, latest: May 31 2022 at 05:30)
• [isabelle] New in the AFP: A Restricted Definition of the... (1 message, latest: May 30 2022 at 11:43)
• [isabelle] New in the AFP: The Plünnecke-Ruzsa Inequality (1 message, latest: May 30 2022 at 07:27)
• [isabelle] print_attribute values (2 messages, latest: May 29 2022 at 09:55)
• [isabelle] New in the AFP: The Sound Automation of Magic ... (1 message, latest: May 27 2022 at 14:02)
• [isabelle] Annoying syntax issue wrt parentheses (8 messages, latest: May 27 2022 at 00:04)
• [isabelle] Discrepancy between "by (metis XXX ...)" and "... (1 message, latest: May 26 2022 at 12:53)
• [isabelle] 3 year postdoc position in computational logic (1 message, latest: May 25 2022 at 12:31)
• [isabelle] Deadline extension: AMAI Special Issue on Symb... (1 message, latest: May 25 2022 at 12:19)
• [isabelle] ITP 2022: Call for Participation (1 message, latest: May 25 2022 at 06:16)
• [isabelle] Second CfP: FM 2023 - 25th International Sympo... (1 message, latest: May 23 2022 at 13:28)
• [isabelle] nil is special (3 messages, latest: May 22 2022 at 05:35)
• [isabelle] ICTAC'22 Last Call For Papers (2 messages, latest: May 20 2022 at 21:54)
• [isabelle] Final CfP: AMAI Special Issue on Symbolic Comp... (1 message, latest: May 20 2022 at 21:54)
• [isabelle] ML Family Workshop 2022: Final Call for Presen... (1 message, latest: May 20 2022 at 21:51)
• [isabelle] "Proofterm.thm_ord" takes a lot of time – can ... (1 message, latest: May 20 2022 at 21:00)
• [isabelle] for the same goal, same proof command behaves ... (3 messages, latest: May 20 2022 at 21:00)
• [isabelle] [CfP] F-IDE 2022: The 7th Workshop on Formal I... (1 message, latest: May 20 2022 at 21:00)
• [isabelle] Computational Logic Autumn Summit, 19-30 Septe... (1 message, latest: May 20 2022 at 20:04)
• [isabelle] Call for Participation - SPIN 2022 - FREE regi... (1 message, latest: May 13 2022 at 08:54)
• [isabelle] Final extension CfP: FMBC 2022 - 4th Internati... (1 message, latest: May 13 2022 at 08:54)
• [isabelle] CICM 2022, Abstract Submnission Deadline Exten... (1 message, latest: May 13 2022 at 06:47)
• [isabelle] iPRA 2022: Deadline extension, final call for ... (1 message, latest: May 12 2022 at 10:18)
• [isabelle] Adding premises to Sledgehammer (2 messages, latest: May 12 2022 at 07:43)
• [isabelle] Deadline extension: SMT Workshop 2022 (1 message, latest: May 11 2022 at 20:48)
• [isabelle] LOPSTR 2022 - Deadline extension! (1 message, latest: May 10 2022 at 15:40)
• [isabelle] 7th SC-Square Workshop 2022 Call for Papers (w... (1 message, latest: May 09 2022 at 18:50)
• [isabelle] New in the AFP: Digit Expansions (1 message, latest: May 09 2022 at 15:40)
• [isabelle] New in the AFP: The Sophomore's Dream (1 message, latest: May 09 2022 at 14:25)
• [isabelle] Women in Logic 2022 - Call for Contributions (1 message, latest: May 09 2022 at 13:27)
• [isabelle] Scottish Programming Languages and Verificatio... (1 message, latest: May 09 2022 at 08:04)
• [isabelle] ICTAC 2022 - CFP - Hybrid - September 27-29,Tb... (2 messages, latest: May 08 2022 at 17:36)
• [isabelle] Lifting and transfer for the topology type (7 messages, latest: May 08 2022 at 17:32)
• [isabelle] New in the AFP: Clique is not solvable by mono... (1 message, latest: May 08 2022 at 12:30)
• [isabelle] Call for papers: Isabelle Workshop 2022 (3 messages, latest: May 07 2022 at 18:54)
• [isabelle] Job announcement: Software FV Engineer at Appl... (1 message, latest: May 06 2022 at 15:22)
• [isabelle] Researcher Formal Verification position at Hen... (1 message, latest: May 06 2022 at 08:28)
• [isabelle] Deadline extension CfP: FMBC 2022 - 4th Intern... (1 message, latest: May 05 2022 at 09:33)
• [isabelle] Inclusion-exclusion principle in Isabelle? (2 messages, latest: May 04 2022 at 16:28)
• [isabelle] CSL'23 - call for papers (1 message, latest: May 04 2022 at 06:59)
• [isabelle] SMT Workshop 2022: Final Call for Papers (1 message, latest: May 02 2022 at 17:12)
• [isabelle] AITP 2022 FINAL CALL FOR CONTRIBUTIONS - EXTEN... (1 message, latest: May 02 2022 at 05:12)
• [isabelle] BCS-FACS evening seminar, 24 June 2022: Alan T... (1 message, latest: May 01 2022 at 22:33)
• [isabelle] New in the AFP: Fisher's Inequality: Linear Al... (1 message, latest: Apr 29 2022 at 17:24)
• [isabelle] Unusual behaviour with Eisbach methods defined... (1 message, latest: Apr 29 2022 at 16:02)
• [isabelle] Second CfP: FMBC 2022 - 4th International Work... (1 message, latest: Apr 27 2022 at 09:51)
• [isabelle] Position of Lecturer or Senior Lecturer in Cyb... (2 messages, latest: Apr 26 2022 at 20:35)
• [isabelle] [fm-announcements] MOVEP: Early-bird rate ends... (1 message, latest: Apr 26 2022 at 14:03)
• [isabelle] LOPSTR 2022 - Final Call for Papers (1 message, latest: Apr 25 2022 at 16:03)
• [isabelle] CICM 2022, 15th Conf. Intelligent Computer Mat... (3 messages, latest: Apr 25 2022 at 15:08)
• [isabelle] Nominal2 manual? (3 messages, latest: Apr 24 2022 at 22:42)
• [isabelle] Call for Presentations: VardiFest22 (1 message, latest: Apr 24 2022 at 01:29)
• [isabelle] JFLA 2022: Call for Participation (in French) (1 message, latest: Apr 22 2022 at 12:45)
• [isabelle] New in the AFP: The Generalized Multiset Order... (1 message, latest: Apr 22 2022 at 09:32)
• [isabelle] [fm-announcements] NFM 2022 - Call for partici... (1 message, latest: Apr 21 2022 at 11:33)
• [isabelle] Formal Methods 2023 -- Joint call for workshop... (1 message, latest: Apr 21 2022 at 11:32)
• [isabelle] SAT/SMT/AR Summer School 2022: August 14-16 (1 message, latest: Apr 20 2022 at 08:03)
• [isabelle] Deadline extended: CfP for the 8th Workshop on... (1 message, latest: Apr 19 2022 at 09:13)
• [isabelle] New in the AFP: "A Combinator Library for Pref... (1 message, latest: Apr 19 2022 at 08:12)
• [isabelle] AFP Data Collection about Important Concepts a... (5 messages, latest: Apr 13 2022 at 11:05)
• [isabelle] 2nd CFP: ThEdu'22 - Theorem-proving Components... (1 message, latest: Apr 12 2022 at 13:48)
• [isabelle] [ICFEM 2022] Deadline extension (1 message, latest: Apr 12 2022 at 11:15)
• [isabelle] MPC 2022 - Deadline extension (1 message, latest: Apr 12 2022 at 11:14)
• [isabelle] Tenure-track assistant professor in Formal Asp... (1 message, latest: Apr 09 2022 at 08:17)
• [isabelle] Running a theory file containing ML code on co... (4 messages, latest: Apr 08 2022 at 15:08)
• [isabelle] cvc4 always crashing (2 messages, latest: Apr 07 2022 at 07:27)
• [isabelle] Vacancy at Lancaster University (Leipzig campu... (1 message, latest: Apr 05 2022 at 13:47)
• [isabelle] Call for papers: 8th Workshop on Practical Asp... (1 message, latest: Apr 05 2022 at 12:57)
• [isabelle] ICTCS'22: preliminary CfP (1 message, latest: Apr 04 2022 at 13:17)
• [isabelle] 7th SC^2 Workshop - Second Call For Papers (1 message, latest: Apr 04 2022 at 12:33)
• [isabelle] Fully Funded PhD Positions in the Safety and S... (1 message, latest: Apr 03 2022 at 15:43)
• [isabelle] [ICFEM 2022] Last CfP (1 message, latest: Apr 03 2022 at 09:18)
• [isabelle] The internal implementation of Isabelle (ML) t... (3 messages, latest: Apr 02 2022 at 13:54)
• [isabelle] Teaching students about Sledgehammer (4 messages, latest: Mar 29 2022 at 21:56)
• [isabelle] New in the AFP: A Naive Prover for First-Order... (1 message, latest: Mar 29 2022 at 12:20)
• [isabelle] Final Call for Papers -- Mathematics of Progra... (1 message, latest: Mar 29 2022 at 10:16)
• [isabelle] PLP 2022 - Call for Papers (1 message, latest: Mar 29 2022 at 10:16)
• [isabelle] New in the AFP: Constructing the Reals as Dede... (1 message, latest: Mar 29 2022 at 06:31)
• [isabelle] First CfP: FMBC 2022 - 4th International Works... (1 message, latest: Mar 28 2022 at 14:52)
• [isabelle] 2nd CfP: AMAI Special Issue on Symbolic Comput... (1 message, latest: Mar 27 2022 at 16:36)
• [isabelle] The latest Apple offerings (4 messages, latest: Mar 24 2022 at 18:57)
• [isabelle] How can I evaluate a function interpreted from... (3 messages, latest: Mar 24 2022 at 12:06)
• [isabelle] 10 fully funded PhD positions at TU Wien (Vien... (1 message, latest: Mar 24 2022 at 12:06)
• [isabelle] CMCS 2022: Call for Participation (1 message, latest: Mar 24 2022 at 12:05)
• [isabelle] ASPOCP 2022 - Call for papers (1 message, latest: Mar 24 2022 at 09:40)
• [isabelle] CSL'23 - Call for workshops (1 message, latest: Mar 24 2022 at 09:40)
• [isabelle] New in the AFP: Ackermann's Function Is Not Pr... (1 message, latest: Mar 24 2022 at 07:19)
• [isabelle] First CFP: FM 2023 - 25th International Sympos... (1 message, latest: Mar 23 2022 at 10:07)
• [isabelle] Wrong semantics for fmul_add in afp/IEEE_Float... (3 messages, latest: Mar 18 2022 at 20:07)
• [isabelle] Showing records countable (4 messages, latest: Mar 17 2022 at 14:03)
• [isabelle] Formal Methods in Computer-Aided Design 2022: ... (1 message, latest: Mar 16 2022 at 16:18)
• [isabelle] new in the AFP: Partial Fraction Expansion of ... (1 message, latest: Mar 16 2022 at 11:44)
• [isabelle] FSCD 2024: Call for Location (1 message, latest: Mar 15 2022 at 13:46)
• [isabelle] Morello: Edinburgh research post on capability... (1 message, latest: Mar 11 2022 at 19:09)
• [isabelle] 8 Positions in AI and in Cyber Security (Chair... (1 message, latest: Mar 09 2022 at 13:59)
• [isabelle] value command failed (2 messages, latest: Mar 09 2022 at 11:00)
• [isabelle] AITP 2022 - Call for Contributions (1 message, latest: Mar 08 2022 at 10:43)
• [isabelle] New in the AFP: The Independence of the Contin... (1 message, latest: Mar 07 2022 at 14:11)
• [isabelle] SMT 2022 - 20th International Workshop on Sati... (1 message, latest: Mar 07 2022 at 11:31)
• [isabelle] 22nd Midlands Graduate School, 10-14 April 202... (1 message, latest: Mar 06 2022 at 21:26)
• [isabelle] New in the AFP: Residuated Transition Systems (1 message, latest: Mar 06 2022 at 20:04)
• [isabelle] New in the AFP: Transitive Models of Fragments... (1 message, latest: Mar 04 2022 at 12:39)
• [isabelle] Call for bids to host ITP 2023 (1 message, latest: Mar 04 2022 at 10:32)
• [isabelle] What characters are permitted in naming lemmas? (3 messages, latest: Mar 04 2022 at 10:29)
• [isabelle] PhD Position in Number Theory and Formalization (1 message, latest: Mar 03 2022 at 19:08)
• [isabelle] quickcheck for datatype t = T "t list" (4 messages, latest: Mar 02 2022 at 16:39)
• [isabelle] About using frule with impI (2 messages, latest: Mar 02 2022 at 11:35)
• [isabelle] printing debug info from generated code execut... (2 messages, latest: Feb 24 2022 at 22:10)
• [isabelle] CFP: Publisher: Springer Nature; Security, Cyb... (1 message, latest: Feb 24 2022 at 17:10)
• [isabelle] Isabelle Performance Benchmark (5 messages, latest: Feb 24 2022 at 16:31)
• [isabelle] 2 is Suc (Suc 0)? (6 messages, latest: Feb 24 2022 at 16:04)
• [isabelle] Document comments after text omitted in PDF ou... (1 message, latest: Feb 23 2022 at 17:09)
• [isabelle] Antiquotation causes type check errors elsewhere (1 message, latest: Feb 23 2022 at 11:44)
• [isabelle] ICGT 2022: Second Call for Papers (1 message, latest: Feb 22 2022 at 10:41)
• [isabelle] New entry in the AFP: Universal Hash Families (1 message, latest: Feb 21 2022 at 19:34)
• [isabelle] New in the AFP: Wetzel's Problem and the Conti... (1 message, latest: Feb 21 2022 at 16:58)
• [isabelle] New AFP entry: First-Order Query Evaluation (1 message, latest: Feb 21 2022 at 06:45)
• [isabelle] Workshop: Machine-Checked Mathematics (1 message, latest: Feb 20 2022 at 13:04)
• [isabelle] Conference announcements in isabelle-users cla... (2 messages, latest: Feb 18 2022 at 12:10)
• [isabelle] Call for Participation: ETAPS Mentoring Worksh... (1 message, latest: Feb 18 2022 at 09:15)
• [isabelle] HOL-TestGen tool running error (1 message, latest: Feb 18 2022 at 01:36)
• [isabelle] quick_and_dirty mode affects regular proofs (i... (1 message, latest: Feb 17 2022 at 15:13)
• [isabelle] New AFP entry Multi-Head Monitoring of Metric ... (1 message, latest: Feb 14 2022 at 18:44)
• [isabelle] How to debug/navigate reflected code (2 messages, latest: Feb 12 2022 at 06:59)
• [isabelle] code_reflect and logical file system confusion (2 messages, latest: Feb 12 2022 at 06:57)
• [isabelle] HOL-Eisbach brings in Pure and confusion (3 messages, latest: Feb 11 2022 at 12:39)
• [isabelle] Potential bug regarding `OF` with match patter... (3 messages, latest: Feb 11 2022 at 10:50)
• [isabelle] Potential bug regarding non-permanent thinning (1 message, latest: Feb 11 2022 at 02:07)
• [isabelle] New in the AFP: First-Order Theory of Rewriting (1 message, latest: Feb 10 2022 at 17:24)
• [isabelle] Broken link in AFP (1 message, latest: Feb 10 2022 at 10:52)
• [isabelle] Shutting down the community wiki - migrate to ... (2 messages, latest: Feb 09 2022 at 15:59)
• [isabelle] Fully funded PhD position on formalization of ... (1 message, latest: Jan 10 2022 at 10:18)
• [isabelle] Associate/Assistant professorship in Copenhage... (1 message, latest: Jan 05 2022 at 11:07)
• [isabelle] New in the AFP: Knight's Tour Revisited Revisited (1 message, latest: Jan 04 2022 at 17:33)
• [isabelle] Changing Options in Isabelle2021-1 (1 message, latest: Jan 04 2022 at 12:34)
• [isabelle] The capability to construct AST from Isabelle ... (1 message, latest: Jan 03 2022 at 10:04)
• [isabelle] Two new AFP entries: Gale-Shapley Algorithm an... (1 message, latest: Jan 03 2022 at 09:17)
• [isabelle] New in the AFP: Regular Tree Relations (1 message, latest: Dec 29 2021 at 12:14)
• [isabelle] New in the AFP: Markov Decision Processes (1 message, latest: Dec 28 2021 at 15:03)
• [isabelle] CFP: ThEdu'22 (1 message, latest: Dec 27 2021 at 18:14)
• [isabelle] Using Isabelle with 'minimal' imports (5 messages, latest: Dec 24 2021 at 16:11)
• [isabelle] Jedit error (3 messages, latest: Dec 23 2021 at 14:06)
• [isabelle] Recursive functions over non datatype input (2 messages, latest: Dec 21 2021 at 11:29)
• [isabelle] Formalizing Axiomatic Systems for Propositiona... (1 message, latest: Dec 21 2021 at 10:46)
• [isabelle] IJCAR 2022 - Call for Papers (1 message, latest: Dec 17 2021 at 11:33)
• [isabelle] Fully (UK Home) Funded PhD Positions in the Sa... (1 message, latest: Dec 15 2021 at 10:37)
• [isabelle] Missing commands in generated AFP websites (2 messages, latest: Dec 14 2021 at 16:44)
• [isabelle] AFP 2021-1 (1 message, latest: Dec 14 2021 at 10:25)
• [isabelle] Announcing Isabelle2021-1 (2 messages, latest: Dec 13 2021 at 20:35)
• [isabelle] new AFP entry: Foundation_of_geometry (1 message, latest: Dec 13 2021 at 03:47)
• [isabelle] new AFP entry: Simplicial Complexes and Boolea... (1 message, latest: Dec 13 2021 at 03:24)
• [isabelle] Semantic subtypes and lifting vs. simple predi... (2 messages, latest: Dec 09 2021 at 11:33)
• [isabelle] Certified Programs and Proofs (CPP) 2022: Call... (2 messages, latest: Dec 09 2021 at 10:26)
• [isabelle] Faculty position at Portland State University (2 messages, latest: Dec 08 2021 at 08:50)
• [isabelle] Isabelle2021-1-RC5: Outdated information about... (2 messages, latest: Dec 07 2021 at 21:18)
• [isabelle] The Undecidability of the Continuum Hypothesis (3 messages, latest: Dec 07 2021 at 08:57)
• [isabelle] adding chained facts to a method (5 messages, latest: Dec 06 2021 at 10:31)
• [isabelle] Isabelle and compiler verification PhD schola... (1 message, latest: Dec 05 2021 at 23:39)
• [isabelle] Isabelle2021-1-RC3: smt (verit) behaves differ... (5 messages, latest: Dec 04 2021 at 22:09)
• [isabelle] Isabelle2021-1-RC5 available for applications (3 messages, latest: Dec 04 2021 at 22:07)
• [isabelle] Break up or down? (1 message, latest: Dec 03 2021 at 13:19)
• [isabelle] Trends in Functional Programming in Education ... (2 messages, latest: Dec 03 2021 at 10:42)
• [isabelle] Isabelle Community Wiki? (2 messages, latest: Nov 30 2021 at 17:10)
• [isabelle] ML Cleanup problems (4 messages, latest: Nov 30 2021 at 14:08)
• [isabelle] Isabelle2021-1-RC3: excessive Poly/ML heapreq... (6 messages, latest: Nov 30 2021 at 11:03)
• [isabelle] Isabelle2021-1-RC3: excessive Poly/ML heap req... (12 messages, latest: Nov 29 2021 at 17:51)
• [isabelle] Isabelle2021-1-RC4 and afp-2021-1 available fo... (5 messages, latest: Nov 28 2021 at 03:09)
• [isabelle] Commandline results for quickcheck / nitpick (3 messages, latest: Nov 28 2021 at 00:03)
• [isabelle] the term export argument in `Assumption.export` (1 message, latest: Nov 27 2021 at 09:14)
• [isabelle] New in the AFP: The Hahn and Jordan Decomposit... (1 message, latest: Nov 26 2021 at 18:21)
• [isabelle] Using the AFP repo as a component (4 messages, latest: Nov 26 2021 at 17:36)
• [isabelle] blast looping and backtracking (4 messages, latest: Nov 26 2021 at 11:19)
• [isabelle] New in the AFP: Exploring Simplified Variants ... (1 message, latest: Nov 26 2021 at 10:59)
• [isabelle] New in the AFP: van Emde Boas Trees (1 message, latest: Nov 26 2021 at 09:50)
• [isabelle] Isabelle2021: cvc4 crashing (fixed) (2 messages, latest: Nov 25 2021 at 15:58)
• [isabelle] Isabelle document generation and ACM and LIPIc... (6 messages, latest: Nov 25 2021 at 11:22)
• [isabelle] Permanent research-intensive academic post: Ve... (1 message, latest: Nov 23 2021 at 10:01)
• [isabelle] Proposal for a proof assistants StackExchange ... (2 messages, latest: Nov 22 2021 at 19:09)
• [isabelle] Troubleshooting a nondeterministic SMT failure (5 messages, latest: Nov 22 2021 at 15:28)
• [isabelle] How can I use Code_Abstract_Nat in Isabelle? (3 messages, latest: Nov 19 2021 at 15:52)
• [isabelle] A rather unusual application of Isabelle, to d... (1 message, latest: Nov 18 2021 at 11:06)
• [isabelle] Isabelle2021-1-RC3: verit errors (4 messages, latest: Nov 17 2021 at 09:31)
• [isabelle] Difference between lemma attribute and declare (1 message, latest: Nov 16 2021 at 12:16)
• [isabelle] CMCS 2022: First Call for Papers (1 message, latest: Nov 16 2021 at 09:18)
• [isabelle] Isabelle2021-1-RC3 sledgehammer works fine on ... (9 messages, latest: Nov 15 2021 at 21:46)
• [isabelle] Isabelle2021-1-RC3 available for testing (3 messages, latest: Nov 15 2021 at 11:09)
• [isabelle] Isabelle2021-1-RC3: OOM Killer? (1 message, latest: Nov 15 2021 at 09:26)
• [isabelle] conversions for symmetric/commutative operators (5 messages, latest: Nov 14 2021 at 20:18)
• [isabelle] Isabelle2021-1-RC3: HELP! Bad context exception (2 messages, latest: Nov 14 2021 at 13:52)
• [isabelle] Isabelle2021-1-RC3: HELP! Bad context exception (2 messages, latest: Nov 14 2021 at 12:08)
• [isabelle] new AFP entry: Automating Public Announcement ... (1 message, latest: Nov 14 2021 at 03:49)
• [isabelle] new AFP entry: Factorization of Polynomials wi... (1 message, latest: Nov 14 2021 at 03:49)
• [isabelle] Domain-specific visual representations of stru... (1 message, latest: Nov 14 2021 at 01:06)
• [isabelle] fork for afp 2021-1 (1 message, latest: Nov 14 2021 at 00:57)
• [isabelle] Theorem Proving Research Associate Position in... (1 message, latest: Nov 14 2021 at 00:16)
• [isabelle] Isabelle2021-1-RC3. Odd sledgehammer proof rec... (1 message, latest: Nov 13 2021 at 23:33)
• [isabelle] Looking for Isabelle experts in the Paris area (1 message, latest: Nov 13 2021 at 12:42)
• [isabelle] Isabelle2021-1-RC3: Isabelle/VSCode extension (1 message, latest: Nov 13 2021 at 11:50)
• [isabelle] Code generation for typedefs with an invariant (6 messages, latest: Nov 12 2021 at 18:36)
• [isabelle] Semantic hyperlinks: Hooray! (2 messages, latest: Nov 11 2021 at 07:59)
• [isabelle] Isabelle2021-1-RC2: Invoking smt-method in the... (7 messages, latest: Nov 10 2021 at 20:01)
• [isabelle] conversions for symmetric/commutative operator... (1 message, latest: Nov 10 2021 at 10:42)
• [isabelle] New in the AFP: Real Exponents as Limits of Ra... (1 message, latest: Nov 09 2021 at 11:50)
• [isabelle] Isabelle2021-1-RC2: Exception when initializin... (3 messages, latest: Nov 09 2021 at 11:42)
• [isabelle] Isabelle2021-1-RC1 (veriT): Abnormal terminati... (3 messages, latest: Nov 08 2021 at 10:02)
• [isabelle] Isabelle2021-1-RC2 available for testing (1 message, latest: Nov 07 2021 at 19:38)
• [isabelle] New in the AFP: Szemerédi's Regularity Lemma (1 message, latest: Nov 07 2021 at 16:40)
• [isabelle] New in the AFP: Registers (1 message, latest: Nov 07 2021 at 10:16)
• [isabelle] s/h: bogus proofs from e (10 messages, latest: Nov 05 2021 at 10:39)
• [isabelle] Isabelle2021-1-RC1: Download for Linux (ARM64) (2 messages, latest: Nov 04 2021 at 10:23)
• [isabelle] Isabelle2021-1-RC1: macOS 12 Monterey (2 messages, latest: Nov 04 2021 at 10:13)
• [isabelle] Isabelle2021-1 on Windows 11 (1 message, latest: Nov 03 2021 at 10:02)
• [isabelle] Isabelle2021-1 on Windows 11 (1 message, latest: Nov 02 2021 at 12:22)
• [isabelle] Isabelle2021-1-RC1: more official status of sn... (1 message, latest: Nov 01 2021 at 22:46)
• [isabelle] Isabelle2021-1-RC1 available for testing (1 message, latest: Nov 01 2021 at 19:35)
• [isabelle] new in the AFP: X86 instruction semantics and ... (1 message, latest: Oct 31 2021 at 04:19)
• [isabelle] Wrong semantics for fmul_add inafp/IEEE_Float... (1 message, latest: Oct 30 2021 at 17:44)
• [isabelle] Deadline extension! Call for Presentations: Pr... (1 message, latest: Oct 30 2021 at 10:18)
• [isabelle] FSCD 2023: Call for Location (1 message, latest: Oct 30 2021 at 10:17)
• [isabelle] Full Professorship for Formal Methods at JKU Linz (1 message, latest: Oct 24 2021 at 11:35)
• [isabelle] Engineer positions for the ProofInUse consortium (1 message, latest: Oct 22 2021 at 14:47)
• [isabelle] New AFP entry Belief Revision Theory (1 message, latest: Oct 22 2021 at 08:58)
• [isabelle] PLMW@POPL 2022: Call for Applications (1 message, latest: Oct 22 2021 at 02:52)
• [isabelle] my Machine Logic blog (1 message, latest: Oct 21 2021 at 11:10)
• [isabelle] New in the AFP:Algebras for Iteration, Infinit... (1 message, latest: Oct 20 2021 at 10:02)
• [isabelle] New in the AFP: Verified Quadratic Virtual Sub... (1 message, latest: Oct 19 2021 at 13:44)
• [isabelle] [Isabelle2021-1-RC0] Simp-rules for bit (1 message, latest: Oct 14 2021 at 13:14)
• [isabelle] signature of ml_antiquotation.ML: inline, valu... (4 messages, latest: Oct 12 2021 at 17:30)
• [isabelle] VerifyThis 2022 --- Call for Problems (1 message, latest: Oct 12 2021 at 17:25)
• [isabelle] usage of Isabelle as a simplifier in batch mode (2 messages, latest: Oct 12 2021 at 15:33)
• [isabelle] Declaration position markup with "notation",b... (1 message, latest: Oct 12 2021 at 13:05)
• [isabelle] "Illegal schematic variable(s) in case" when u... (3 messages, latest: Oct 11 2021 at 16:11)
• [isabelle] is this expected behaviour? (file attached) (2 messages, latest: Oct 09 2021 at 11:40)
• [isabelle] joint postdoc at Carnegie Mellon (1 message, latest: Oct 08 2021 at 13:42)
• [isabelle] Adhoc Overloading and Coercion not working well (2 messages, latest: Oct 06 2021 at 12:39)
• [isabelle] Second and Final Call for Submissions: Program... (1 message, latest: Oct 06 2021 at 09:41)
• [isabelle] Second and Final Call for Presentations: PriSC... (1 message, latest: Oct 06 2021 at 09:41)
• [isabelle] new AFP entry: FOL_Axiomatic (1 message, latest: Oct 04 2021 at 23:55)
• [isabelle] macOS app launcher (5 messages, latest: Oct 04 2021 at 21:02)
• [isabelle] Phantom locale notations (4 messages, latest: Oct 04 2021 at 13:43)
• [isabelle] Isabelle2021-1-RC0 available for experiments (2 messages, latest: Oct 04 2021 at 10:26)
• [isabelle] How to verify properties of simple SML programs (4 messages, latest: Oct 03 2021 at 05:17)
• [isabelle] FSCD 2022: First Call for Papers (1 message, latest: Oct 02 2021 at 09:18)
• [isabelle] Naming policy of sessions in the AFP (5 messages, latest: Sep 30 2021 at 10:22)
• [isabelle] Proofterms and rule attributes (1 message, latest: Sep 30 2021 at 09:48)
• [isabelle] Declarations not activated by Interpretation.i... (5 messages, latest: Sep 29 2021 at 10:25)
• [isabelle] [TFP'22] first call for papers: Trends in Func... (1 message, latest: Sep 28 2021 at 10:16)
• [isabelle] Performance considerations of locales (5 messages, latest: Sep 27 2021 at 09:50)
• [isabelle] Performance bottleneck in Theory_Data.merge (5 messages, latest: Sep 27 2021 at 07:50)
• [isabelle] New in the AFP: A Formalization of Weighted Pa... (1 message, latest: Sep 26 2021 at 13:49)
• [isabelle] Post-doctoral Research Fellow / Research Fello... (1 message, latest: Sep 24 2021 at 03:54)
• [isabelle] New in the AFP: Complex Bounded Operators (1 message, latest: Sep 20 2021 at 08:02)
• [isabelle] FSCD 2022: Final Call for Workshops (deadline:... (1 message, latest: Sep 18 2021 at 09:56)
• [isabelle] Declarations not activated byInterpretation.i... (1 message, latest: Sep 17 2021 at 13:29)
• [isabelle] PhD position at the University of Copenhagen (1 message, latest: Sep 15 2021 at 19:25)
• [isabelle] Call for Presentations: PriSC 2022 @ POPL 2022 (1 message, latest: Sep 15 2021 at 08:15)
• [isabelle] Exception using setup_lifting (1 message, latest: Sep 15 2021 at 08:14)
• [isabelle] posdoctoral position in Prague (1 message, latest: Sep 14 2021 at 12:13)
• [isabelle] seven new AFP entries (1 message, latest: Sep 14 2021 at 09:26)
• [isabelle] 2nd CfP - ThEdu'21 post-proceedings at EPTCS (1 message, latest: Sep 13 2021 at 08:32)
• [isabelle] Using the Parallel library (5 messages, latest: Sep 12 2021 at 14:38)
• [isabelle] EuroProofNet - Call for Working Group membersh... (2 messages, latest: Sep 10 2021 at 10:41)
• [isabelle] Superscript argument to a function (7 messages, latest: Sep 08 2021 at 10:23)
• [isabelle] 30 months postdoctoral research position at Un... (1 message, latest: Sep 08 2021 at 07:03)
• [isabelle] New in the AFP: A data flow analysis algorithm... (1 message, latest: Sep 07 2021 at 19:07)
• [isabelle] a lemma for List (2 messages, latest: Sep 07 2021 at 16:01)
• [isabelle] new in the AFP: Minkowski Spacetime (1 message, latest: Sep 06 2021 at 14:05)
• [isabelle] New AFP entry: Logging-independent Message Ano... (1 message, latest: Sep 05 2021 at 07:45)
• [isabelle] Call for Participation: In-person School on Ve... (1 message, latest: Sep 04 2021 at 09:54)
• [isabelle] New in the AFP: Solving Cubic and Quartic Equa... (1 message, latest: Sep 03 2021 at 16:14)
• [isabelle] cvc4 prover always crashing (2 messages, latest: Sep 03 2021 at 00:15)
• [isabelle] New in the AFP: Combinatorial Design Theory (1 message, latest: Sep 02 2021 at 12:42)
• [isabelle] New in the AFP: The Theorem of Three Circles (1 message, latest: Sep 01 2021 at 12:00)
• [isabelle] Issue launching jEdit for multiple Isabelle ve... (4 messages, latest: Sep 01 2021 at 08:39)
• [isabelle] Ordering of the complex numbers (6 messages, latest: Sep 01 2021 at 06:41)
• [isabelle] Call for Participation: HotSpot 2021 (1 message, latest: Aug 27 2021 at 09:08)
• [isabelle] Research Assistant/Associate at Department of ... (1 message, latest: Aug 27 2021 at 09:08)
• [isabelle] Research position at fortiss, Munich (2 messages, latest: Aug 26 2021 at 09:56)
• [isabelle] Document antiquotation for referring to lemmas (2 messages, latest: Aug 23 2021 at 12:48)
• [isabelle] semantic selection in Isabelle/jEdit (4 messages, latest: Aug 22 2021 at 21:23)
• [isabelle] Reporting nitpick counterexample where Isabell... (4 messages, latest: Aug 20 2021 at 11:11)
• [isabelle] How to debug Match exceptions when using code_... (2 messages, latest: Aug 20 2021 at 10:31)
• [isabelle] syntax for algorithm definition? (3 messages, latest: Aug 19 2021 at 09:52)
• [isabelle] Certified Programs and Proofs (CPP) 2022: Fina... (1 message, latest: Aug 19 2021 at 07:00)
• [isabelle] New in the AFP: Fresh identifiers (1 message, latest: Aug 18 2021 at 10:31)
• [isabelle] try0 says "Please inform Tobias Nipkow" (1 message, latest: Aug 14 2021 at 03:08)
• [isabelle] Rewriting bitwise in the new Word library (2 messages, latest: Aug 12 2021 at 16:08)
• [isabelle] IJCAR 2022 - Call for Workshops,Tutorials and... (1 message, latest: Aug 11 2021 at 09:55)
• [isabelle] Professorship (W3) for Theoretical Informatics... (1 message, latest: Aug 10 2021 at 09:37)
• [isabelle] New in the AFP: Relational Forests (1 message, latest: Aug 08 2021 at 09:07)
• [isabelle] Call for Participation: CALCO & MFPS 2021 (1 message, latest: Aug 05 2021 at 16:11)
• [isabelle] Apparent deadlock issue with Isabelle/JEdit (1 message, latest: Aug 04 2021 at 13:06)
• [isabelle] Announcement: Verified SAT Solver ISASAT wins ... (3 messages, latest: Jul 28 2021 at 21:12)
• [isabelle] Call for papers - ThEdu'21 post-proceedings at... (1 message, latest: Jul 27 2021 at 16:59)
• [isabelle] Isabelle Zulip Chat (3 messages, latest: Jul 26 2021 at 11:20)
• [isabelle] CICM 2021, July 26-31, Call for online partici... (1 message, latest: Jul 26 2021 at 10:10)
• [isabelle] Postdoctoral Opening at the University of Minn... (1 message, latest: Jul 23 2021 at 09:16)
• [isabelle] Turning intervals into lists: upt and upto (7 messages, latest: Jul 19 2021 at 08:47)
• [isabelle] Postdoc position: Formal methods in control (M... (1 message, latest: Jul 16 2021 at 14:44)
• [isabelle] Lazy Code Generation (2 messages, latest: Jul 16 2021 at 09:29)
• [isabelle] Nitpick Codatatype - No Counterexample found (2 messages, latest: Jul 14 2021 at 12:34)
• [isabelle] Primrec abstracts over the wrong variable (4 messages, latest: Jul 14 2021 at 08:06)
• [isabelle] New in the AFP: Finitely_Generated_Abelian_Groups (1 message, latest: Jul 13 2021 at 18:50)
• [isabelle] Sorting algorithms in the AFP (5 messages, latest: Jul 09 2021 at 18:20)
• [isabelle] New AFP entry SpecCheck (1 message, latest: Jul 08 2021 at 19:30)
• [isabelle] JFLA 2022: Call for papers (in French) (1 message, latest: Jul 08 2021 at 14:22)
• [isabelle] How to retrieve theorems defined in ML (1 message, latest: Jul 08 2021 at 13:35)
• [isabelle] Extreme processing time for function definition (7 messages, latest: Jul 08 2021 at 10:13)
• [isabelle] Printing a term without abbreviations/notation (5 messages, latest: Jul 07 2021 at 14:13)
• [isabelle] FSCD 2021: Final Call for (Online) Participati... (1 message, latest: Jul 07 2021 at 08:37)
• [isabelle] FMBC 2021 - Call for Participation (1 message, latest: Jul 06 2021 at 09:03)
• [isabelle] Second Call for Papers (Deadline Extension): F... (1 message, latest: Jul 03 2021 at 09:26)
• [isabelle] Fixed-term research position at Mitsubishi Ele... (1 message, latest: Jul 03 2021 at 09:26)
• [isabelle] Call for Workshops - FLoC 2022 — The 2022 Fede... (1 message, latest: Jul 01 2021 at 14:33)
• [isabelle] SMT Workshop 2021: Call for Participation (1 message, latest: Jun 30 2021 at 08:51)
• [isabelle] Call for Participation - SPIN 2021 (1 message, latest: Jun 30 2021 at 08:51)
• [isabelle] Incompatibility between code generation, HOL-L... (2 messages, latest: Jun 30 2021 at 07:25)
• [isabelle] PDF file not generated (4 messages, latest: Jun 28 2021 at 21:49)
• [isabelle] Last Call for Participation: 12th Internationa... (1 message, latest: Jun 26 2021 at 13:20)
• [isabelle] Two new AFP entries: "Public Announcement Logi... (1 message, latest: Jun 25 2021 at 10:12)
• [isabelle] New in the AFP: Van der Waerden's Theorem (1 message, latest: Jun 23 2021 at 10:52)
• [isabelle] SErAPIS update, June 2021 (MAJOR update) (1 message, latest: Jun 23 2021 at 10:16)
• [isabelle] Job offer: 3 year research engineer in static ... (1 message, latest: Jun 22 2021 at 13:20)
• [isabelle] Active Area for jEdit Console (1 message, latest: Jun 21 2021 at 09:10)
• [isabelle] WiL'21 Final Call for Participation (1 message, latest: Jun 21 2021 at 08:52)
• [isabelle] New in the AFP: A Shorter Compiler Correctness... (1 message, latest: Jun 21 2021 at 07:12)
• [isabelle] SCSS 2021: call for short and work-in-progress... (1 message, latest: Jun 19 2021 at 10:45)
• [isabelle] Add markup to term annotations (1 message, latest: Jun 19 2021 at 10:45)
• [isabelle] Industry researchers and engineer sought for n... (1 message, latest: Jun 19 2021 at 10:42)
• [isabelle] Proof Ground 2021 Call for Participation (1 message, latest: Jun 18 2021 at 12:47)
• [isabelle] Update on the SErAPIS search engine: New videos (1 message, latest: Jun 17 2021 at 16:19)
• [isabelle] PhD position on Embedded Systems Verification ... (1 message, latest: Jun 16 2021 at 09:44)
• [isabelle] FSCD 2021: Call for (Online) Participation (1 message, latest: Jun 15 2021 at 08:08)
• [isabelle] Execute typedef Definition (2 messages, latest: Jun 14 2021 at 10:35)
• [isabelle] Call for Papers: Fifth Workshop on Formal Math... (1 message, latest: Jun 14 2021 at 07:01)
• [isabelle] Question about some projects to work on (1 message, latest: Jun 13 2021 at 20:14)
• [isabelle] Code equations for Rep in lift_definition with... (2 messages, latest: Jun 13 2021 at 17:56)
• [isabelle] Profiling time? (4 messages, latest: Jun 12 2021 at 10:24)
• [isabelle] FVPS 2021: Deadline Extension (June 25, 2021) (1 message, latest: Jun 12 2021 at 09:20)
• [isabelle] CADE 2021 call for participation (1 message, latest: Jun 10 2021 at 05:21)
• [isabelle] The instructions in AFP's "Using Entries" do n... (8 messages, latest: Jun 07 2021 at 09:24)
• [isabelle] [Second Call for Papers] Formal Verification o... (1 message, latest: Jun 07 2021 at 09:02)
• [isabelle] VS Code extension (5 messages, latest: Jun 05 2021 at 11:34)
• [isabelle] build output (2 messages, latest: Jun 05 2021 at 11:27)
• [isabelle] [Call for Participation] 12th International Sc... (2 messages, latest: Jun 04 2021 at 10:07)
• [isabelle] Research position in Formal Verification at HE... (1 message, latest: Jun 04 2021 at 10:06)
• [isabelle] New AFP entry: Lifting the Exponent (1 message, latest: May 31 2021 at 18:41)
• [isabelle] CALCO 2021: Deadline extension and invited spe... (1 message, latest: May 30 2021 at 11:06)
• [isabelle] PhD position on program verification in Coq (1 message, latest: May 28 2021 at 09:03)
• [isabelle] Generating set comprehensions as part of a syn... (2 messages, latest: May 27 2021 at 12:58)
• [isabelle] New in the AFP: Combinatorics on Words (1 message, latest: May 26 2021 at 10:18)
• [isabelle] Concerning Fun.swap (3 messages, latest: May 22 2021 at 06:26)
• [isabelle] PhD position using Isabelle in Saarbrücken (1 message, latest: May 20 2021 at 16:26)
• [isabelle] Cannot build HOL.Complex_Main (2 messages, latest: May 20 2021 at 11:26)
• [isabelle] SCSS 2021: deadline extension (1 message, latest: May 20 2021 at 09:00)
• [isabelle] Bitblasting via SAT and Argo (3 messages, latest: May 18 2021 at 13:43)
• [isabelle] elimination rule for length s = Suc n (3 messages, latest: May 17 2021 at 15:49)
• [isabelle] Exhaustiveness of Pure.type (3 messages, latest: May 17 2021 at 13:56)
• [isabelle] [Call for Papers] Formal Verification of Physi... (1 message, latest: May 17 2021 at 10:07)
• [isabelle] RV'21 Call for Papers (with an Extended Deadline) (1 message, latest: May 16 2021 at 16:52)
• [isabelle] isabelle ghc_setup (2 messages, latest: May 16 2021 at 14:18)
• [isabelle] Generate fun/datatype definition in ML (3 messages, latest: May 15 2021 at 10:14)
• [isabelle] New in the AFP: Hensel's Lemma for the p-adic ... (1 message, latest: May 14 2021 at 16:02)
• [isabelle] Questions regarding endomorphisms of real norm... (2 messages, latest: May 14 2021 at 15:28)
• [isabelle] Last CfP: SCSS 2021 (1 message, latest: May 14 2021 at 09:07)
• [isabelle] 5 permanent positions (lecturer, senior lectur... (1 message, latest: May 13 2021 at 22:36)
• [isabelle] First Call for Papers: Formal Methods Teaching... (1 message, latest: May 13 2021 at 08:26)
• [isabelle] CALCO 2021: Second call for papers (1 message, latest: May 11 2021 at 09:57)
• [isabelle] postdoc position (6 years) in CL group in Inns... (1 message, latest: May 11 2021 at 09:56)
• [isabelle] FMBC 2021 - Final Call for Papers (Deadline ex... (1 message, latest: May 10 2021 at 08:57)
• [isabelle] New book: Functional Algorithms, Verified! (1 message, latest: May 10 2021 at 06:51)
• [isabelle] Postdoc in Computing Science with a Specialisa... (1 message, latest: May 05 2021 at 12:33)
• [isabelle] High CPU usage on PolyML subprocess (Pure/HOL)... (5 messages, latest: May 04 2021 at 09:48)
• [isabelle] New in the AFP: Regression Test Selection (1 message, latest: May 03 2021 at 18:12)
• [isabelle] A Redesign of the Archive of Formal Proofs (1 message, latest: May 03 2021 at 13:00)
• [isabelle] Recurring error from Isabelle Syslog (6 messages, latest: May 03 2021 at 12:04)
• [isabelle] parse_translation does not detect changes in t... (10 messages, latest: May 02 2021 at 13:29)
• [isabelle] SMT 2021 Workshop: Deadline Extension to May 7 (1 message, latest: May 01 2021 at 10:03)
• [isabelle] How to get TopLevel.state from the theorem str... (1 message, latest: Apr 28 2021 at 22:43)
• [isabelle] Atb.: Is it possible to use QRHL tool without ... (1 message, latest: Apr 28 2021 at 17:08)
• [isabelle] Can QRHL tool be used without QRHL theories, f... (1 message, latest: Apr 28 2021 at 16:35)
• [isabelle] Generic Lemma about Sums of Powers divided by ... (1 message, latest: Apr 28 2021 at 14:24)
• [isabelle] Term to be evaluated contains free dictionaries (4 messages, latest: Apr 28 2021 at 11:08)
• [isabelle] NASA Formal Methods 2021: Call for (virtual)p... (1 message, latest: Apr 28 2021 at 09:18)
• [isabelle] Two new AFP entries: Gale-Stewart games and Is... (1 message, latest: Apr 28 2021 at 08:36)
• [isabelle] Failed call to isabelle jedit -R with code gen... (5 messages, latest: Apr 28 2021 at 08:02)
• [isabelle] new in the AFP: The BKR Decision Procedure for... (1 message, latest: Apr 25 2021 at 15:40)
• [isabelle] Using the global context when performing synta... (1 message, latest: Apr 25 2021 at 09:17)
• [isabelle] FMBC 2021 - 3rd Call for Papers (Deadline exte... (1 message, latest: Apr 25 2021 at 09:17)
• [isabelle] "Simple Type Theory is not too Simple": commen... (15 messages, latest: Apr 24 2021 at 22:41)
• [isabelle] 7th International Workshop on Proof eXchange f... (3 messages, latest: Apr 22 2021 at 15:12)
• [isabelle] 2021 Conference on Intelligent Computer Mathem... (1 message, latest: Apr 20 2021 at 08:49)
• [isabelle] SPIN 2021 - Final Call for Papers (1 message, latest: Apr 20 2021 at 08:49)
• [isabelle] Women in Logic 2021 - Call for Participation (1 message, latest: Apr 20 2021 at 08:49)
• [isabelle] [CFP] Logical Frameworks and Meta-Languages: T... (5 messages, latest: Apr 20 2021 at 08:49)
• [isabelle] Announcing SErAPIS: a new search engine for Is... (3 messages, latest: Apr 20 2021 at 08:48)
• [isabelle] Symbolic execution in Isabelle. (5 messages, latest: Apr 19 2021 at 20:24)
• [isabelle] CfP: Logical Frameworks and Meta-Languages: Th... (1 message, latest: Apr 19 2021 at 14:32)
• [isabelle] Lemma like shiftr_bl but for sshiftr in Word L... (2 messages, latest: Apr 18 2021 at 22:22)
• [isabelle] New in the AFP: Formalization of Timely Datafl... (1 message, latest: Apr 16 2021 at 05:47)
• [isabelle] Quickcheck reports an incorrect counterexample (3 messages, latest: Apr 16 2021 at 05:28)
• [isabelle] Datatype definition can be slow (10 messages, latest: Apr 16 2021 at 02:39)
• [isabelle] SMT 2021 Workshop: Final Call for Papers (1 message, latest: Apr 14 2021 at 09:10)
• [isabelle] Issues with locale interpretation (3 messages, latest: Apr 11 2021 at 17:01)
• [isabelle] FMBC: Second Call for Papers (1 message, latest: Apr 10 2021 at 09:18)
• [isabelle] New in the AFP: Grothendieck's Schemes in Alge... (1 message, latest: Apr 09 2021 at 13:39)
• [isabelle] Editing the Isabelle Wiki (3 messages, latest: Apr 08 2021 at 10:40)
• [isabelle] Possible problem with floating-point addition ... (4 messages, latest: Apr 07 2021 at 15:35)
• [isabelle] Announcement: Isabelle/DOF 1.1.0 (1 message, latest: Apr 06 2021 at 18:47)
• [isabelle] export code checking OCaml: zarith not found (3 messages, latest: Apr 06 2021 at 14:09)
• [isabelle] Results — Survey on the AFP (1 message, latest: Apr 06 2021 at 09:12)
• [isabelle] Parsing term is easy with Scala, can similar a... (2 messages, latest: Apr 05 2021 at 00:09)
• [isabelle] Pārs.: Parsing term is easy with Scala, can s... (2 messages, latest: Apr 04 2021 at 22:49)
• [isabelle] New AFP entry: Information Flow Control via De... (1 message, latest: Apr 01 2021 at 10:14)
• [isabelle] UNIF 2021: second call for papers (1 message, latest: Apr 01 2021 at 09:26)
• [isabelle] Evaluation of definitions defined inside a locale (5 messages, latest: Mar 31 2021 at 05:55)
• [isabelle] 2nd CfP: SCSS 2021 (1 message, latest: Mar 30 2021 at 08:44)
• [isabelle] Deadline Extension: April 5th, 20201,14th Con... (1 message, latest: Mar 30 2021 at 08:44)
• [isabelle] hd and last of Nil (15 messages, latest: Mar 29 2021 at 11:36)
• [isabelle] Proof Ground 2021 - Call for Problems (1 message, latest: Mar 29 2021 at 09:17)
• [isabelle] Morello: Edinburgh research posts on capabilit... (1 message, latest: Mar 29 2021 at 09:09)
• [isabelle] I completed mmt_import but now I have some que... (2 messages, latest: Mar 28 2021 at 13:35)
• [isabelle] Pārs.: How to see the names of all active Is... (1 message, latest: Mar 27 2021 at 14:41)
• [isabelle] Atb.: How to see the names of all active Isabe... (1 message, latest: Mar 27 2021 at 14:22)
• [isabelle] CFP ICTCS 2021 - 22th Italian Conference on Th... (1 message, latest: Mar 26 2021 at 10:56)
• [isabelle] Specifying a Universal Property in a localede... (2 messages, latest: Mar 23 2021 at 19:43)
• [isabelle] C-to-Isabelle multiple external files (4 messages, latest: Mar 23 2021 at 10:20)
• [isabelle] How to see the names of all active Isabelle se... (2 messages, latest: Mar 22 2021 at 15:42)
• [isabelle] Call for Papers: HotSpot 2021 (1 message, latest: Mar 22 2021 at 10:23)
• [isabelle] Formal algorithms in Isabelle - is it OK to sp... (2 messages, latest: Mar 20 2021 at 19:46)
• [isabelle] \isakeyword in bold? (1 message, latest: Mar 18 2021 at 10:15)
• [isabelle] New in the AFP: Constructive Cryptography in H... (1 message, latest: Mar 18 2021 at 07:52)
• [isabelle] Remaining uses of "isabelle process" and "isab... (9 messages, latest: Mar 17 2021 at 15:03)
• [isabelle] 21st Midlands Graduate School in the Foundatio... (2 messages, latest: Mar 17 2021 at 11:04)
• [isabelle] 14th Conference on Intelligent Computer Mathem... (3 messages, latest: Mar 17 2021 at 10:02)
• [isabelle] A lemma about remove1 (3 messages, latest: Mar 16 2021 at 07:18)
• [isabelle] Specifying a Universal Property in a locale de... (1 message, latest: Mar 15 2021 at 19:36)
• [isabelle] building the document in Windows from Isabelle... (2 messages, latest: Mar 15 2021 at 16:14)
• [isabelle] Entire theory in JSON forma using scala-isabelle? (3 messages, latest: Mar 15 2021 at 12:17)
• [isabelle] Pārs.: Entire theory in JSON forma using scal... (1 message, latest: Mar 14 2021 at 16:54)
• [isabelle] New in the AFP: Two algorithms based on modula... (1 message, latest: Mar 14 2021 at 11:13)
• [isabelle] Request for feedback: dedicated session or AFP... (6 messages, latest: Mar 13 2021 at 13:46)
• [isabelle] ML questions (3 messages, latest: Mar 13 2021 at 11:16)
• [isabelle] Research Programmer in HoTT and Cubical Type T... (1 message, latest: Mar 13 2021 at 11:12)
• [isabelle] Lecturer in Verification position at Universit... (1 message, latest: Mar 13 2021 at 01:23)
• [isabelle] keywords "spark_open" :: thy_load (spark_siv) (6 messages, latest: Mar 12 2021 at 16:28)
• [isabelle] New in the AFP: The Hermite–Lindemann–Weierstr... (1 message, latest: Mar 12 2021 at 14:38)
• [isabelle] Well-behaved MacOS application for Isabelle 2021 (1 message, latest: Mar 11 2021 at 17:26)
• [isabelle] Some more polishing of the multiset theory (5 messages, latest: Mar 11 2021 at 10:50)
• [isabelle] by fact and try0 (2 messages, latest: Mar 09 2021 at 16:38)
• [isabelle] New in the AFP: Quantum projective measurements (1 message, latest: Mar 09 2021 at 15:00)
• [isabelle] Structure of Proofs (3 messages, latest: Mar 08 2021 at 17:17)
• [isabelle] Troubles building Pure; can't find Foreign.bui... (2 messages, latest: Mar 06 2021 at 23:16)
• [isabelle] Nitpick finds counterexample to proven lemma (2 messages, latest: Mar 06 2021 at 09:03)
• [isabelle] New in the AFP: Mereology (1 message, latest: Mar 05 2021 at 12:09)
• [isabelle] Isabelle 2021 Word Library (3 messages, latest: Mar 05 2021 at 11:12)
• [isabelle] Python client to Isabelle server (4 messages, latest: Mar 04 2021 at 22:30)
• [isabelle] ATVA 2021 - Second Call for Papers (1 message, latest: Mar 04 2021 at 16:51)
• [isabelle] SPIN 2021 - Deadline extension to April 20 (1 message, latest: Mar 04 2021 at 10:24)
• [isabelle] Towards a formalization of elements of the fou... (1 message, latest: Mar 03 2021 at 20:13)
• [isabelle] Fixing type variables in locales (6 messages, latest: Mar 03 2021 at 14:14)
• [isabelle] Code generation for a subtype with free_constr... (1 message, latest: Mar 02 2021 at 11:55)
• [isabelle] Working with list symmetry (Attributes for the... (1 message, latest: Mar 02 2021 at 10:33)
• [isabelle] Error in DockerHub documentation (8 messages, latest: Mar 01 2021 at 14:09)
• [isabelle] New in the AFP: The Sunflower Lemma of Erdős a... (1 message, latest: Mar 01 2021 at 12:37)
• [isabelle] AFP instructions (20 messages, latest: Feb 28 2021 at 21:25)
• [isabelle] FMBC 2021: First Call for Papers (1 message, latest: Feb 28 2021 at 10:48)
• [isabelle] SMT 2021 Workshop: Second Call for Papers (1 message, latest: Feb 28 2021 at 10:48)
• [isabelle] New in the AFP: Formal Puiseux Series (12 messages, latest: Feb 26 2021 at 16:28)
• [isabelle] FMCAD 2021: First Call for Papers (1 message, latest: Feb 26 2021 at 10:34)
• [isabelle] New in the AFP: A Verified Imperative Implemen... (1 message, latest: Feb 26 2021 at 06:27)
• [isabelle] Weak lemma: HOL-Algebra.Multiplicative_Group.g... (2 messages, latest: Feb 25 2021 at 16:50)
• [isabelle] RC5: Syntactic class bit_operations is gone (6 messages, latest: Feb 25 2021 at 16:40)
• [isabelle] Berghofer's program extraction mechanism and c... (4 messages, latest: Feb 25 2021 at 15:55)
• [isabelle] Postdoc/phd positions in ERC project "Certifie... (1 message, latest: Feb 25 2021 at 12:43)
• [isabelle] Bill McCune PhD Award in Automated Reasoning,... (1 message, latest: Feb 24 2021 at 14:40)
• [isabelle] Request for TTP and PTT Interfaces (2 messages, latest: Feb 23 2021 at 12:58)
• [isabelle] AFP 2021 (2 messages, latest: Feb 23 2021 at 11:56)
• [isabelle] Unfixed variables in "define" command (8 messages, latest: Feb 22 2021 at 14:39)
• [isabelle] Announcing Isabelle2021 (1 message, latest: Feb 21 2021 at 20:50)
• [isabelle] First day with HOL/Isabelle (4 messages, latest: Feb 21 2021 at 20:04)
• [isabelle] Predicate Compiler fails with "No specificatio... (6 messages, latest: Feb 21 2021 at 19:21)
• [isabelle] Relation of function absent from Main (3 messages, latest: Feb 20 2021 at 21:57)
• [isabelle] 2nd CfP ThEdu'21 (1 message, latest: Feb 19 2021 at 17:35)
• [isabelle] Syntax proposal: multiway if (8 messages, latest: Feb 19 2021 at 15:37)
• [isabelle] unused_thms in composed theorems (1 message, latest: Feb 19 2021 at 14:04)
• [isabelle] Assistant/Associate Professor positions in Edi... (1 message, latest: Feb 17 2021 at 09:59)
• [isabelle] Yet another Isabelle-Course available (1 message, latest: Feb 17 2021 at 09:02)
• [isabelle] Conflict of type arities: What are the constra... (4 messages, latest: Feb 17 2021 at 00:48)
• [isabelle] Isabelle2021-RC3 New failure mode for "try"/sl... (5 messages, latest: Feb 16 2021 at 13:30)
• [isabelle] Weird nesting of Quantifiers (5 messages, latest: Feb 16 2021 at 12:27)
• [isabelle] Rewrites for a sublocale with UNIV as the carr... (7 messages, latest: Feb 16 2021 at 10:36)
• [isabelle] Open pdf files from Isabelle File Browser (2 messages, latest: Feb 16 2021 at 09:56)
• [isabelle] RC5: Short experience report (4 messages, latest: Feb 15 2021 at 13:36)
• [isabelle] RC5: Sledgehammer and HOL-Library.Word problems (3 messages, latest: Feb 15 2021 at 09:57)
• [isabelle] Isabelle2021-RC6 available for applications (1 message, latest: Feb 14 2021 at 18:43)
• [isabelle] Isabelle2021-RC5: support for Apple Silicon (2 messages, latest: Feb 13 2021 at 12:57)
• [isabelle] CFP SAT-2021: Deadline March 19th (1 message, latest: Feb 12 2021 at 10:45)
• [isabelle] PhD position in Formal Methods/Decompilation a... (1 message, latest: Feb 12 2021 at 10:45)
• [isabelle] isabelle scala_project and Gradle / IntelliJ s... (1 message, latest: Feb 11 2021 at 13:44)
• [isabelle] Comparing Isabelle/Scala with scala-isabelle. ... (5 messages, latest: Feb 11 2021 at 13:22)
• [isabelle] FSCD 2021: Extended deadline (Abstract: Februa... (1 message, latest: Feb 11 2021 at 10:05)
• [isabelle] New in the AFP: The Laws of Large Numbers (1 message, latest: Feb 11 2021 at 05:40)
• [isabelle] Boolos's Curious Inference (Speed-Up) in Isabe... (2 messages, latest: Feb 10 2021 at 13:40)
• [isabelle] Isabelle2021-RC5 available for applications (1 message, latest: Feb 08 2021 at 21:43)
• [isabelle] Atb.: Isabelle code for getting in-memory repr... (1 message, latest: Feb 05 2021 at 22:39)
• [isabelle] Isabelle code for getting in-memory representa... (5 messages, latest: Feb 05 2021 at 20:56)
• [isabelle] Isabelle2021-RC1 - Any way to limit "veriT" me... (15 messages, latest: Feb 05 2021 at 13:36)
• [isabelle] CfP: SCSS 2021 (1 message, latest: Feb 03 2021 at 09:54)
• [isabelle] Isabelle logo terms of use (2 messages, latest: Feb 02 2021 at 19:55)
• [isabelle] Call for Papers: Tests and Proofs 2021 (TAP 20... (1 message, latest: Feb 02 2021 at 09:37)
• [isabelle] New in the AFP: Solution to the xkcd Blue Eyes... (1 message, latest: Feb 01 2021 at 17:24)
• [isabelle] Isabelle2021-RC0: Java/VM monitor (8 messages, latest: Feb 01 2021 at 15:34)
• [isabelle] Isabelle2021-RC3: Java 11 (LTS) vs. Java 15 (MTS) (3 messages, latest: Feb 01 2021 at 15:09)
• [isabelle] Isabelle2021-RC2: slight regression in HTML ou... (4 messages, latest: Feb 01 2021 at 14:59)
• [isabelle] Isabelle2021-RC4: bundling of Naproche-SAD (1 message, latest: Feb 01 2021 at 14:51)
• [isabelle] Isabelle2021-RC4 available for applications (1 message, latest: Feb 01 2021 at 14:46)
• [isabelle] New in the AFP: a port of GeoCoq (1 message, latest: Feb 01 2021 at 12:05)
• [isabelle] Pārs.: Isabelle code for getting in-memory re... (1 message, latest: Jan 31 2021 at 02:50)
• [isabelle] Transfer Question (1 message, latest: Jan 31 2021 at 01:55)
• [isabelle] "Files and Folders" permissions cannot be granted (4 messages, latest: Jan 30 2021 at 00:16)
• [isabelle] Configurable proposition grammar root symbol f... (1 message, latest: Jan 28 2021 at 17:55)
• [isabelle] UTF8 chars behavior (2 messages, latest: Jan 28 2021 at 11:12)
• [isabelle] CFP: Workshop on the Role of Mathematical Reas... (1 message, latest: Jan 26 2021 at 23:15)
• [isabelle] Isabelle2021-RC3: macOS access to Documents fo... (13 messages, latest: Jan 26 2021 at 22:19)
• [isabelle] Isabelle C wrapper [was Isabelle2021-RC3: macO... (5 messages, latest: Jan 26 2021 at 21:08)
• [isabelle] Isabelle2021-RC2: Problems downloading (9 messages, latest: Jan 26 2021 at 17:50)
• [isabelle] AFP 2021 preparations (5 messages, latest: Jan 25 2021 at 21:50)
• [isabelle] Isabelle2021-RC2: improved HTML presentation (7 messages, latest: Jan 25 2021 at 20:50)
• [isabelle] rewrite, subst, uses and sequential compositio... (4 messages, latest: Jan 25 2021 at 20:07)
• [isabelle] rewrite, subst,uses and sequential compositio... (1 message, latest: Jan 24 2021 at 23:13)
• [isabelle] Isabelle2021-RC3: update of Scala, but not Ope... (2 messages, latest: Jan 24 2021 at 21:00)
• [isabelle] Bug report Isabelle 2019 and Isabelle 2020 (9 messages, latest: Jan 24 2021 at 19:29)
• [isabelle] Isabelle2021-RC2, Isabelle/jEdit getting sluggish (3 messages, latest: Jan 24 2021 at 18:59)
• [isabelle] Isabelle2021-RC3 available for testing (1 message, latest: Jan 24 2021 at 18:39)
• [isabelle] [Lambda Days + TFP + TFPIE 2021] call for part... (1 message, latest: Jan 23 2021 at 10:53)
• [isabelle] CADE-28: $n$th call for papers (1 message, latest: Jan 22 2021 at 20:05)
• [isabelle] Some lemmas with a combinatoric flavor (3 messages, latest: Jan 20 2021 at 12:51)
• [isabelle] CFP: HCSS 2021 - High Confidence Software and ... (1 message, latest: Jan 20 2021 at 10:11)
• [isabelle] Console errors in AFP build after push (3 messages, latest: Jan 19 2021 at 18:00)
• [isabelle] Blog entry: Release Candidates for Isabelle2021 (1 message, latest: Jan 19 2021 at 15:44)
• [isabelle] Translating from Isar to ML? (6 messages, latest: Jan 19 2021 at 15:19)
• [isabelle] ATVA 2021 - Call for Papers (1 message, latest: Jan 19 2021 at 08:13)
• [isabelle] Derive bounded sets from extended nat (3 messages, latest: Jan 18 2021 at 22:06)
• [isabelle] Epigenetics and similar Phenomena (1 message, latest: Jan 17 2021 at 11:57)
• [isabelle] ITP 2021: Third Call for Papers (1 message, latest: Jan 16 2021 at 16:10)
• [isabelle] Two questions about the availability of certai... (3 messages, latest: Jan 16 2021 at 14:15)
• [isabelle] Isabelle keywords (2 messages, latest: Jan 16 2021 at 13:03)
• [isabelle] Some lemmas on factorial rings (2 messages, latest: Jan 14 2021 at 15:28)
• [isabelle] Lemma suggestion to Function_Algebras (3 messages, latest: Jan 14 2021 at 15:21)
• [isabelle] SMT 2021 Workshop: Call for Papers (1 message, latest: Jan 14 2021 at 10:50)
• [isabelle] New AFP entry: JinjaDCI: a Java semantics with... (1 message, latest: Jan 13 2021 at 09:37)
• [isabelle] Updating AFP entry (3 messages, latest: Jan 12 2021 at 23:27)
• [isabelle] New in the AFP: The HOL-CSP Refinement Toolkit (1 message, latest: Jan 12 2021 at 12:10)
• [isabelle] Isabelle 2021-RC1: Problem with fonts in jEdit (3 messages, latest: Jan 11 2021 at 17:53)
• [isabelle] Detecting undefined (6 messages, latest: Jan 11 2021 at 17:48)
• [isabelle] brute force search in lists (2 messages, latest: Jan 11 2021 at 08:11)
• [isabelle] Variable both free and bound?! (5 messages, latest: Jan 10 2021 at 18:34)
• [isabelle] Debug facilities of locales (2 messages, latest: Jan 10 2021 at 18:27)
• [isabelle] F-IDE 2021 - 2nd Call for Papers (1 message, latest: Jan 10 2021 at 18:24)
• [isabelle] Issue with Isabelle/jEdit in fullscreen mode i... (3 messages, latest: Jan 10 2021 at 16:09)
• [isabelle] Isabelle2021-RC1 - editing below sometimes cau... (4 messages, latest: Jan 10 2021 at 15:58)
• [isabelle] Isabelle2021-RC2 available for testing (1 message, latest: Jan 10 2021 at 15:53)
• [isabelle] Strange "Tactic failed" error in lift_definiti... (1 message, latest: Jan 10 2021 at 10:38)
• [isabelle] Isabelle2021-RC1 - sledgehammer suggestion "by... (1 message, latest: Jan 09 2021 at 15:21)
• [isabelle] [TFP'21] final call for papers: Trends in Func... (1 message, latest: Jan 09 2021 at 12:36)
• [isabelle] Isabelle2021-RC1 - error highlighting (4 messages, latest: Jan 08 2021 at 20:18)
• [isabelle] Custom fonts in browser_info html? (3 messages, latest: Jan 08 2021 at 15:29)
• [isabelle] fully funded PhD position on verification of i... (1 message, latest: Jan 07 2021 at 10:19)
• [isabelle] Questions about "transfer" (4 messages, latest: Jan 06 2021 at 23:31)
• [isabelle] Call for Papers: Tests and Proofs 2021 (TAP 2021) (1 message, latest: Jan 06 2021 at 10:08)
• [isabelle] ITP2021: Second Call for Workshops (Deadline 1... (1 message, latest: Jan 06 2021 at 10:08)
• [isabelle] Questionnaire on deployed verified systems (1 message, latest: Jan 05 2021 at 12:24)
• [isabelle] FSCD 2021: Second Call for Papers (1 message, latest: Jan 05 2021 at 10:11)
• [isabelle] Research assistant/associate position at Imper... (1 message, latest: Jan 05 2021 at 10:11)
• [isabelle] Several questions about the availability of ce... (9 messages, latest: Jan 04 2021 at 17:23)
• [isabelle] Go-to-definition doesn't work when exploring l... (2 messages, latest: Jan 04 2021 at 12:37)
• [isabelle] low-level code formalisations in Isabelle (1 message, latest: Jan 04 2021 at 08:46)
• [isabelle] Sledgehammer errors (Isabelle 2020) (2 messages, latest: Jan 03 2021 at 17:19)
• [isabelle] CfP Theorem Proving Components for Educational... (1 message, latest: Jan 03 2021 at 16:34)
• [isabelle] sledgehammer (or Z3) internal error (1 message, latest: Jan 03 2021 at 12:00)
• [isabelle] Any fans of "try"? (1 message, latest: Jan 03 2021 at 11:53)
• [isabelle] Apple switching to ARM (1 message, latest: Jan 03 2021 at 11:38)
• [isabelle] Bootstrap problem in Isabelle2021-RC1: Consume... (2 messages, latest: Jan 03 2021 at 11:27)
• [isabelle] Using LaTeX output print mode for source text (2 messages, latest: Jan 02 2021 at 10:48)
• [isabelle] Question about "try" and future tasks (2 messages, latest: Jan 02 2021 at 10:36)
• [isabelle] quote in mixfix annotation (2 messages, latest: Jan 02 2021 at 10:11)
• [isabelle] Cannot load theory when building (2 messages, latest: Jan 02 2021 at 10:04)
• [isabelle] Another ZF entry for the AFP (1 message, latest: Dec 28 2020 at 10:54)
• [isabelle] Isabelle2021-RC1 available for testing (1 message, latest: Dec 27 2020 at 19:15)
• [isabelle] CPP 2021: Call for Participation and Lightning... (1 message, latest: Dec 22 2020 at 18:37)
• [isabelle] New in the AFP: Topological semantics for para... (1 message, latest: Dec 22 2020 at 13:12)
• [isabelle] [TFPIE'21] Second Call For Papers: Trends in F... (1 message, latest: Dec 19 2020 at 11:07)
• [isabelle] Question regarding nitpick (5 messages, latest: Dec 19 2020 at 10:03)
• [isabelle] Deadline extension: AMAI Special Issue on Theo... (1 message, latest: Dec 14 2020 at 11:01)
• [isabelle] Invitation to celebrate the World Logic Day di... (1 message, latest: Dec 11 2020 at 09:24)
• [isabelle] FSCD 2021: Third Call for Workshop Proposals -... (1 message, latest: Dec 10 2020 at 11:53)
• [isabelle] Postdoc and research engineer positions in Sem... (1 message, latest: Dec 09 2020 at 18:13)
• [isabelle] [TFP'21] second call for papers: Trends in Fun... (1 message, latest: Dec 09 2020 at 11:15)
• [isabelle] take_all is equivalence (2 messages, latest: Dec 08 2020 at 21:06)
• [isabelle] New AFP entry: Full name: Relational Minimum S... (1 message, latest: Dec 08 2020 at 12:15)
• [isabelle] new in the AFP: The Verification of Cryptograp... (1 message, latest: Dec 07 2020 at 12:18)
• [isabelle] Lean Together 2021: January 4-7, Call for Part... (1 message, latest: Dec 07 2020 at 10:22)
• [isabelle] Postdoc and PhD Positions @ Iowa State University (1 message, latest: Dec 06 2020 at 11:37)
• [isabelle] Isabelle2021-RC0 available for early experiments (2 messages, latest: Dec 04 2020 at 12:50)
• [isabelle] PriSC 2021: call for participation and short t... (1 message, latest: Dec 04 2020 at 10:18)
• [isabelle] ITP2021: Call for Workshops (1 message, latest: Dec 04 2020 at 10:18)
• [isabelle] Efficient code for inductive predicates (4 messages, latest: Dec 03 2020 at 10:10)
• [isabelle] Sub/superscripts in document preparation (4 messages, latest: Dec 02 2020 at 18:49)
• [isabelle] 2nd CfP: AMAI Special Issue on Theoretical and... (1 message, latest: Dec 02 2020 at 09:40)
• [isabelle] New in the AFP: Finite Map Extras (1 message, latest: Dec 01 2020 at 21:32)
• [isabelle] Formalising Ordinal Partition Relations (1 message, latest: Dec 01 2020 at 16:07)
• [isabelle] FSCD 2021: Second Call for Workshop Proposals ... (1 message, latest: Dec 01 2020 at 13:16)
• [isabelle] State of affairs with words (1 message, latest: Nov 30 2020 at 18:57)
• [isabelle] Unknown JAVA_HOME -- Java unavailable (2 messages, latest: Nov 30 2020 at 13:06)
• [isabelle] Final Deadline - Survey on the AFP (1 message, latest: Nov 30 2020 at 11:30)
• [isabelle] Observations on ZF (5 messages, latest: Nov 30 2020 at 10:32)
• [isabelle] fully funded PhD position at University of She... (1 message, latest: Nov 30 2020 at 10:01)
• [isabelle] New in the AFP: Isabelle Marries Dirac: a Libr... (1 message, latest: Nov 30 2020 at 09:09)
• [isabelle] ITP 2021 : Second Call for Papers (1 message, latest: Nov 30 2020 at 08:54)
• [isabelle] NASA Formal Methods Symposium (NFM2021) -- Fin... (1 message, latest: Nov 28 2020 at 09:22)
• [isabelle] new in the AFP (1 message, latest: Nov 27 2020 at 14:10)
• [isabelle] superfluous assumptions in comm_append_are_rep... (3 messages, latest: Nov 26 2020 at 18:31)
• [isabelle] Pretty-printing primed identifiers (1 message, latest: Nov 26 2020 at 11:28)
• [isabelle] Looking for partner to teach course on Isabell... (1 message, latest: Nov 25 2020 at 10:02)
• [isabelle] Bug? Or still just confusing correct behavior? (1 message, latest: Nov 21 2020 at 05:25)
• [isabelle] two proof-assistant friendly posts of Lecturer... (1 message, latest: Nov 20 2020 at 13:11)
• [isabelle] Another Issue with Isabelle/jEdit with macOS B... (5 messages, latest: Nov 20 2020 at 11:07)
• [isabelle] Counting lines of code/definition vs proof? (2 messages, latest: Nov 19 2020 at 13:55)
• [isabelle] Manually using a SideKick parser (2 messages, latest: Nov 19 2020 at 11:47)
• [isabelle] Local varification/unvarification in Isabelle/ML? (1 message, latest: Nov 18 2020 at 00:09)
• [isabelle] Code generation for non-terminating functions (3 messages, latest: Nov 17 2020 at 19:57)
• [isabelle] Typos in lemma names (2 messages, latest: Nov 15 2020 at 14:02)
• [isabelle] NFM2021 - Second Call for Papers (1 message, latest: Nov 14 2020 at 11:50)
• [isabelle] Weak lemma:HOL-Algebra.Multiplicative_Group.g... (1 message, latest: Nov 13 2020 at 18:30)
• [isabelle] New in the AFP: AI planning (1 message, latest: Nov 13 2020 at 13:24)
• [isabelle] ROOT file for imported theory (3 messages, latest: Nov 13 2020 at 07:17)
• [isabelle] scala-isabelle: A library for interfacing with... (1 message, latest: Nov 12 2020 at 13:23)
• [isabelle] Survey on the AFP (1 message, latest: Nov 11 2020 at 09:59)
• [isabelle] Implicit exporting of goal state by different ... (7 messages, latest: Nov 10 2020 at 10:11)
• [isabelle] AutoCorres 1.7 and CParser 1.17 for Isabelle2020 (1 message, latest: Nov 10 2020 at 02:20)
• [isabelle] How do I set --maxheap greater than 16G on Linux? (4 messages, latest: Nov 07 2020 at 22:14)
• [isabelle] Definitional axioms in Isabelle/ML? (2 messages, latest: Nov 07 2020 at 19:12)
• [isabelle] Improvement suggestion for isabelle process (2 messages, latest: Nov 07 2020 at 16:31)
• [isabelle] Call for Papers - SPIN 2021 (1 message, latest: Nov 07 2020 at 10:32)
• [isabelle] Document preparation from within Isabelle/jEdit (5 messages, latest: Nov 06 2020 at 22:50)
• [isabelle] FSCD 2021: First Call for Papers (1 message, latest: Nov 06 2020 at 13:32)
• [isabelle] Code generation: transitive closure of inducti... (5 messages, latest: Nov 04 2020 at 20:21)
• [isabelle] General timeout for tactics (9 messages, latest: Nov 04 2020 at 19:18)
• [isabelle] pat_completeness exception (1 message, latest: Nov 03 2020 at 12:50)
• [isabelle] Performance problem with Simpl and Isabelle si... (1 message, latest: Nov 01 2020 at 11:46)
• [isabelle] Sledgehammer proof reconstruction failed (2 messages, latest: Oct 31 2020 at 08:50)
• [isabelle] Name clash in "let" definitions (4 messages, latest: Oct 29 2020 at 11:02)
• [isabelle] FSCD 2021: Call for Workshop Proposals (1 message, latest: Oct 28 2020 at 11:35)
• [isabelle] New in the AFP: A Sound Type System for Physic... (1 message, latest: Oct 28 2020 at 11:29)
• [isabelle] writing a proof method after "qed" (4 messages, latest: Oct 28 2020 at 10:54)
• [isabelle] Second Call for Presentations: PriSC 2021 @ PO... (1 message, latest: Oct 28 2020 at 09:23)
• [isabelle] CADE-28: Call for Papers, Workshops,Tutorials... (1 message, latest: Oct 21 2020 at 11:32)
• [isabelle] Survey Paper (4 messages, latest: Oct 20 2020 at 13:09)
• [isabelle] Research position in Formal Verification (m/f/... (1 message, latest: Oct 20 2020 at 12:08)
• [isabelle] Benchmark suite for Isabelle's `rewrite` tactic (2 messages, latest: Oct 19 2020 at 15:49)
• [isabelle] make Isabelle accessible? (1 message, latest: Oct 19 2020 at 08:28)
• [isabelle] Error in Eisbach syntax diagram (2 messages, latest: Oct 19 2020 at 00:57)
• [isabelle] scope of facts arising from `subgoal` (3 messages, latest: Oct 17 2020 at 22:19)
• [isabelle] Weak lemmas in HOL-Analysis.Affine (6 messages, latest: Oct 17 2020 at 13:29)
• [isabelle] clashes in _graph names generated by mutual re... (1 message, latest: Oct 15 2020 at 21:17)
• [isabelle] Degree of an almost everywhere constant function (2 messages, latest: Oct 15 2020 at 14:47)
• [isabelle] list_all vs set membership (4 messages, latest: Oct 15 2020 at 08:20)
• [isabelle] PhD and Postdoc positions at the University of... (1 message, latest: Oct 09 2020 at 20:13)
• [isabelle] CfP: AMAI Special Issue on Theoretical and Pra... (1 message, latest: Oct 08 2020 at 10:44)
• [isabelle] finite order allows maxima (12 messages, latest: Oct 07 2020 at 19:50)
• [isabelle] Duplicate algebra tactic (1 message, latest: Oct 07 2020 at 14:13)
• [isabelle] Questions on locales - structure keyword and l... (1 message, latest: Oct 07 2020 at 09:00)
• [isabelle] Unnecessary assumption in HOL-Analysis.Convex.... (1 message, latest: Oct 06 2020 at 09:21)
• [isabelle] Unnecessary assumption inHOL-Analysis.Convex.... (1 message, latest: Oct 06 2020 at 09:03)
• [isabelle] How to make Eisbach's match functionality avai... (2 messages, latest: Oct 05 2020 at 22:42)
• [isabelle] 16 inch MacBook Pro benchmarks (2 messages, latest: Sep 29 2020 at 18:44)
• [isabelle] Minimal system requirements for Isabelle? (3 messages, latest: Sep 28 2020 at 10:49)
• [isabelle] NASA Formal Methods 2021 - First Call for Papers (1 message, latest: Sep 25 2020 at 09:33)
• [isabelle] update Isabelle2019->20, session (2 messages, latest: Sep 25 2020 at 08:44)
• [isabelle] A question about the submission guidelines for... (7 messages, latest: Sep 22 2020 at 02:15)
• [isabelle] New in the AFP: Extended Finite State Machines (1 message, latest: Sep 19 2020 at 06:22)
• [isabelle] A bundle of ATP entries (1 message, latest: Sep 18 2020 at 14:45)
• [isabelle] CPP 2021 abstract deadline due very soon (1 message, latest: Sep 16 2020 at 17:45)
• [isabelle] FMCAD'20 (Sept 21 to 24) - Call for Participation (1 message, latest: Sep 09 2020 at 08:28)
• [isabelle] cartouches and outer syntax (7 messages, latest: Sep 08 2020 at 10:10)
• [isabelle] More on "References about mistakes and gaps in... (2 messages, latest: Sep 08 2020 at 09:11)
• [isabelle] Postdoc position on Formal Methods and Testing... (1 message, latest: Sep 04 2020 at 09:14)
• [isabelle] New in the AFP: inductive inference of recursi... (1 message, latest: Sep 02 2020 at 11:29)
• [isabelle] New AFP entry: Putting the `K' into Bird's der... (1 message, latest: Sep 02 2020 at 10:27)
• [isabelle] linarith_split_limit_exceeded (current value i... (4 messages, latest: Sep 01 2020 at 19:31)
• [isabelle] Isabelle proving theorem with translation (1 message, latest: Sep 01 2020 at 11:14)
• [isabelle] Numbers reported in "Timing" panel (6 messages, latest: Sep 01 2020 at 10:44)
• [isabelle] Strange behaviour of subst/EqSubst.eqsubst_tac (3 messages, latest: Aug 31 2020 at 20:35)
• [isabelle] Isabelle document fails with non-descriptive e... (3 messages, latest: Aug 31 2020 at 14:59)
• [isabelle] New in the AFP: Practical Algebraic Calculus C... (1 message, latest: Aug 31 2020 at 13:01)
• [isabelle] Tracing resolution proofs (3 messages, latest: Aug 31 2020 at 12:22)
• [isabelle] Add comments to the text generated by induct rule (1 message, latest: Aug 27 2020 at 12:43)
• [isabelle] New in the AFP: Relational Disjoint-Set Forests (1 message, latest: Aug 26 2020 at 12:49)
• [isabelle] List minimality proof (4 messages, latest: Aug 26 2020 at 08:26)
• [isabelle] LFMTP 2020 Post-Proceedings: Call for Papers (1 message, latest: Aug 26 2020 at 01:19)
• [isabelle] Handmade transfer rules not invoked (2 messages, latest: Aug 25 2020 at 17:24)
• [isabelle] Unfold short tactics in Isar. (blast, etc) (18 messages, latest: Aug 24 2020 at 13:23)
• [isabelle] Postdocs available in formal analysis of code ... (1 message, latest: Aug 23 2020 at 20:17)
• [isabelle] 16‑inch MacBook Pro (2 messages, latest: Aug 23 2020 at 19:32)
• [isabelle] A suggestion: call eval with try0 (2 messages, latest: Aug 21 2020 at 21:02)
• [isabelle] A question about an article about Isabelle/HOL/ZF (3 messages, latest: Aug 21 2020 at 20:56)
• [isabelle] counter-intuitive definition of the lexicograp... (2 messages, latest: Aug 21 2020 at 08:33)
• [isabelle] Translation of TPTP to Isabelle/HOL? (1 message, latest: Aug 21 2020 at 07:44)
• [isabelle] Translation of Isabelle/ZF statements into met... (3 messages, latest: Aug 20 2020 at 14:35)
• [isabelle] Notation for Pure.all may not work. Bug or fea... (2 messages, latest: Aug 20 2020 at 12:16)
• [isabelle] CADE-28 Call for Papers, Workshops, Tutorials,... (1 message, latest: Aug 19 2020 at 09:46)
• [isabelle] New AFP entry: Ordinal Partitions (1 message, latest: Aug 18 2020 at 10:31)
• [isabelle] Certified Programs and Proofs (CPP) 2021: Fina... (1 message, latest: Aug 18 2020 at 01:33)
• [isabelle] Code generation of a definition obtained throu... (2 messages, latest: Aug 17 2020 at 17:50)
• [isabelle] Issue with pattern_aliases and let (3 messages, latest: Aug 17 2020 at 13:11)
• [isabelle] AFP/Containers, "HOL-Library.Numeral_Type", co... (4 messages, latest: Aug 16 2020 at 13:57)
• [isabelle] New AFP entry: Amicable Numbers (1 message, latest: Aug 15 2020 at 08:18)
• [isabelle] Duplicate fact declaration "RBT.color.simps" v... (3 messages, latest: Aug 14 2020 at 13:58)
• [isabelle] Union of RBT sets (2 messages, latest: Aug 13 2020 at 11:17)
• [isabelle] Unbound schematic variable: ?thesis (4 messages, latest: Aug 08 2020 at 10:10)
• [isabelle] Accessing the proof context from ML (4 messages, latest: Aug 07 2020 at 17:04)
• [isabelle] How to edit the Isabelle sources? (2 messages, latest: Aug 05 2020 at 14:40)
• [isabelle] Cl-isabelle-users Digest, Vol 182, Issue 4 (1 message, latest: Aug 05 2020 at 12:44)
• [isabelle] Isabelle build failure for ’threads=1’ (2 messages, latest: Aug 05 2020 at 09:50)
• [isabelle] Exporting local setup to global context (3 messages, latest: Aug 05 2020 at 09:50)
• [isabelle] [Isabelle] Isabelle proving theorem with trans... (1 message, latest: Aug 05 2020 at 09:43)
• [isabelle] New in the AFP: The Chandy--Lamport Distribute... (1 message, latest: Aug 04 2020 at 11:49)
• [isabelle] Record update syntax (8 messages, latest: Aug 03 2020 at 14:14)
• [isabelle] Unexpected behaviour of lemmas x = ... for A (1 message, latest: Jul 29 2020 at 12:02)
• [isabelle] Isabelle standard mathematics library, HOL-Ana... (10 messages, latest: Jul 28 2020 at 15:30)
• [isabelle] Various "models" of extended reals and impacts... (9 messages, latest: Jul 28 2020 at 09:36)
• [isabelle] New AFP entry: Relational Characterisations of... (1 message, latest: Jul 28 2020 at 07:59)
• [isabelle] Rosetta Code (7 messages, latest: Jul 28 2020 at 00:51)
• [isabelle] new bibitems in document preparation (1 message, latest: Jul 27 2020 at 10:52)
• [isabelle] Representing type dependencies in Isabelle/HOL... (1 message, latest: Jul 25 2020 at 20:51)
• [isabelle] Standard group theory in Isabelle/HOL and in d... (1 message, latest: Jul 24 2020 at 14:37)
• [isabelle] Importing from session 2019 vs. 2020 (1 message, latest: Jul 24 2020 at 13:58)
• [isabelle] Standard group theory in Isabelle/HOL – Isabel... (7 messages, latest: Jul 24 2020 at 08:50)
• [isabelle] Summer School on Programming Languages and Ver... (1 message, latest: Jul 23 2020 at 08:40)
• [isabelle] ML style "functors" for Isabelle theories? (3 messages, latest: Jul 21 2020 at 22:37)
• [isabelle] Isabelle standard mathematics library,HOL-Ana... (1 message, latest: Jul 21 2020 at 20:38)
• [isabelle] get set of (proper) divisors for a specific nu... (5 messages, latest: Jul 20 2020 at 15:50)
• [isabelle] FTfJP 2020 (virtual) - Call for Participation ... (1 message, latest: Jul 17 2020 at 07:46)
• [isabelle] File antiquotation broken after Theory.join_th... (2 messages, latest: Jul 16 2020 at 21:07)
• [isabelle] Folding abbreviations with TYPE(_) parameters (1 message, latest: Jul 14 2020 at 12:29)
• stream events (1 message, latest: Jul 13 2020 at 21:03)

Last updated: Aug 15 2022 at 02:13 UTC