Stream: Mirror: Isabelle Users Mailing List

Topics:

• [isabelle] Trying to understand how to prove an equivalence (2 messages, latest: Sep 02 2026 at 10:17)
• [isabelle] New in the AFP: The Fundamental Group of the C... (1 message, latest: Sep 02 2026 at 08:57)
• [isabelle] Isabelle2026-RC0: macOS ARM vs. Intel (5 messages, latest: Aug 30 2026 at 19:51)
• [isabelle] CfP postproceedings ThEdu'26 (1 message, latest: Aug 30 2026 at 10:33)
• [isabelle] Build of AFP entry PAPP_Impossibility failed (1 message, latest: Aug 29 2026 at 14:45)
• [isabelle] Hooks that nudge LLM coding agents toward sled... (3 messages, latest: Aug 28 2026 at 13:39)
• [isabelle] Is there a "timed" method? (8 messages, latest: Aug 27 2026 at 15:46)
• [isabelle] New in the AFP: Trace Based Semantics for Rely... (1 message, latest: Aug 26 2026 at 08:45)
• [isabelle] New in the AFP: Multitape TMs (1 message, latest: Aug 26 2026 at 06:37)
• [isabelle] Theorem Proving and Artificial Intelligence (11 messages, latest: Aug 25 2026 at 16:42)
• [isabelle] Isabelle2026-RC0 available for experimentation (2 messages, latest: Aug 25 2026 at 09:20)
• [isabelle] New in the AFP: Miquel (1 message, latest: Aug 23 2026 at 15:04)
• [isabelle] new in the AFP: Laurent Series Expansions on a... (1 message, latest: Aug 23 2026 at 10:34)
• [isabelle] Browser-based automated proof search for Isa... (1 message, latest: Aug 22 2026 at 11:02)
• [isabelle] length (4 messages, latest: Aug 19 2026 at 11:51)
• [isabelle] Call for Nominations: POPL 2027 Artifact Evalu... (1 message, latest: Aug 18 2026 at 18:23)
• [isabelle] Isabelle2026-RC0.app on managed macOS machine (5 messages, latest: Aug 18 2026 at 14:57)
• [isabelle] ANU Logic Summer School, 7–18 December 2026 (1 message, latest: Aug 17 2026 at 07:47)
• [isabelle] Browser-based automated proof search for Isabe... (1 message, latest: Aug 16 2026 at 15:35)
• [isabelle] New in the AFP: First-Order Methods for Smooth... (1 message, latest: Aug 13 2026 at 06:06)
• [isabelle] CfP: Special Issue on Formal Methods and Inter... (1 message, latest: Aug 09 2026 at 18:44)
• [isabelle] New in the AFP: A deep embedding of HOL in HOL... (1 message, latest: Aug 07 2026 at 14:37)
• [isabelle] New in the AFP: Cost-Preserving Single-Source ... (1 message, latest: Aug 07 2026 at 14:27)
• [isabelle] New in the AFP: Completeness of the Q0 Higher-... (1 message, latest: Aug 06 2026 at 16:04)
• [isabelle] Isabelle and Varto solve the complete PutnamBe... (2 messages, latest: Aug 05 2026 at 11:12)
• [isabelle] New in the AFP: The Wallace--Simson Line Theor... (1 message, latest: Aug 05 2026 at 08:53)
• [isabelle] PhD Position in Resilient Machine Learning and... (1 message, latest: Aug 02 2026 at 21:28)
• [isabelle] Hybrid Isabelle Workshop at FLoC / Lisboa (1 message, latest: Jul 23 2026 at 20:44)
• [isabelle] New in the AFP: Counterexample to the Jacobian... (1 message, latest: Jul 21 2026 at 19:57)
• [isabelle] Executability of ^* (1 message, latest: Jul 21 2026 at 16:27)
• [isabelle] sublocale declaration question (2 messages, latest: Jul 21 2026 at 11:42)
• [isabelle] [BUG] Delay.run() rethrows exception, killing ... (7 messages, latest: Jul 20 2026 at 22:03)
• [isabelle] [ISSUE] XML.Output.string(null) appends litera... (4 messages, latest: Jul 20 2026 at 21:37)
• [isabelle] New in the AFP: Termination Restricted to Righ... (1 message, latest: Jul 17 2026 at 19:36)
• [isabelle] FSCD 2026: Free online participation, 20 - 23 ... (1 message, latest: Jul 16 2026 at 18:13)
• [isabelle] New in the AFP: Conway's Circle Theorem (1 message, latest: Jul 15 2026 at 15:48)
• [isabelle] VeTSS Summer School 2026 (registration closes ... (1 message, latest: Jul 14 2026 at 09:58)
• [isabelle] New in the AFP: Chevalley-Warning and Equality... (1 message, latest: Jul 14 2026 at 09:17)
• [isabelle] New in the AFP: MSO in HOL by Christoph Benzmü... (1 message, latest: Jul 13 2026 at 12:39)
• [isabelle] New in the AFP: Polynomial Commitment Schemes ... (1 message, latest: Jul 13 2026 at 12:36)
• [isabelle] PIDE MCP: Connecting AI Agents to Isabelle (4 messages, latest: Jul 13 2026 at 08:51)
• [isabelle] Isabelle theory name clash (2 messages, latest: Jul 13 2026 at 08:12)
• [isabelle] Strange effect when matching (intro) + lambda ... (1 message, latest: Jul 11 2026 at 12:00)
• [isabelle] Arithmetic Simplifier Loop (6 messages, latest: Jul 10 2026 at 18:50)
• [isabelle] Hexcitment in the AFP (1 message, latest: Jul 08 2026 at 22:04)
• [isabelle] "Type variable has two distinct sorts" excepti... (1 message, latest: Jul 08 2026 at 14:21)
• [isabelle] New in the AFP: Height Bounds for Height-Balan... (1 message, latest: Jul 07 2026 at 19:57)
• [isabelle] Isabelle2025-2 Download Link Broken (5 messages, latest: Jul 07 2026 at 19:42)
• [isabelle] New in the AFP: Freiman’s 3k−4 Theorem (1 message, latest: Jul 07 2026 at 07:03)
• [isabelle] New in the AFP: Correctness and Complexity of ... (1 message, latest: Jul 06 2026 at 16:16)
• [isabelle] New in the AFP: Certified Infinite Descent Cri... (1 message, latest: Jul 05 2026 at 18:18)
• [isabelle] New in the AFP: Axiomatic theory of hereditari... (1 message, latest: Jul 05 2026 at 15:24)
• [isabelle] Problem with abstract types (2 messages, latest: Jul 04 2026 at 09:36)
• [isabelle] New in the AFP: Formalization of 3-independenc... (1 message, latest: Jul 04 2026 at 07:15)
• [isabelle] veriT (6 messages, latest: Jul 03 2026 at 18:37)
• [isabelle] Extended deadline (July 31, 2026): Nominations... (1 message, latest: Jul 02 2026 at 11:05)
• [isabelle] New in the AFP: Lower-Bound Certificates for O... (9 messages, latest: Jun 30 2026 at 20:05)
• [isabelle] 1st CFP - CPP 2027 - Certified Programs and Pr... (2 messages, latest: Jun 30 2026 at 15:22)
• [isabelle] Problem with mlton component (2 messages, latest: Jun 29 2026 at 19:19)
• [isabelle] New in the AFP: Greedy Algorithms for Cardinal... (1 message, latest: Jun 29 2026 at 11:45)
• [isabelle] GitHub mirror-afp-2025-2 (3 messages, latest: Jun 28 2026 at 15:55)
• [isabelle] New in the AFP: Perron's Formula (1 message, latest: Jun 26 2026 at 12:56)
• [isabelle] Noon in the AFP: ML-Lex and ML-Yacc for Isabelle (2 messages, latest: Jun 25 2026 at 14:49)
• [isabelle] Rewriting with Quasi-AC operators? (2 messages, latest: Jun 24 2026 at 12:43)
• [isabelle] Nominations for the AMS Milestone Prize in For... (1 message, latest: Jun 23 2026 at 11:27)
• [isabelle] HOL-Analysis changes: Incomplete NEWS (3 messages, latest: Jun 22 2026 at 11:06)
• [isabelle] Mathematics for AI (1 message, latest: Jun 19 2026 at 08:49)
• [isabelle] New in the AFP: The Detour Calculus (1 message, latest: Jun 18 2026 at 13:44)
• [isabelle] New in the AFP: Formalization of Weighted Sets (1 message, latest: Jun 17 2026 at 16:59)
• [isabelle] New in the AFP: A Formalization of the Exponen... (1 message, latest: Jun 16 2026 at 15:55)
• [isabelle] postdoc position in Nancy, France (2 messages, latest: Jun 16 2026 at 13:01)
• [isabelle] New in the AFP: The Dottie Number (1 message, latest: Jun 16 2026 at 12:23)
• [isabelle] Lecturer positions in Leeds (1 message, latest: Jun 15 2026 at 18:03)
• [isabelle] PhD position in AI4Math at Chalmers (1 message, latest: Jun 15 2026 at 13:47)
• [isabelle] VSTTE 2026: Second Call for Papers and WIP Pre... (1 message, latest: Jun 15 2026 at 09:45)
• [isabelle] New in the AFP: Countable Multisets (1 message, latest: Jun 14 2026 at 10:43)
• [isabelle] New in the AFP: Fair Games Theorem (1 message, latest: Jun 12 2026 at 15:41)
• [isabelle] New in the AFP: Vosper's Theorem and the Cauch... (1 message, latest: Jun 12 2026 at 10:12)
• [isabelle] How formal verification makes AWS Nitro the fi... (2 messages, latest: Jun 11 2026 at 17:18)
• [isabelle] New in the AFP: Feuerbach's Theorem (1 message, latest: Jun 11 2026 at 15:56)
• [isabelle] Funded Master's positions in symbolic computat... (1 message, latest: Jun 11 2026 at 08:00)
• [isabelle] `before_command` handled differently in scala/... (1 message, latest: Jun 11 2026 at 07:10)
• [isabelle] New in the AFP (1 message, latest: Jun 10 2026 at 16:00)
• [isabelle] Auto-formalisation + document preparation (1 message, latest: Jun 10 2026 at 13:47)
• [isabelle] New in the AFP: Labelled Natural Deduction (1 message, latest: Jun 05 2026 at 17:40)
• [isabelle] New in the AFP: Mechanized Metasemantics of Mo... (1 message, latest: Jun 05 2026 at 16:06)
• [isabelle] A blueprint for formal verification of Apple c... (4 messages, latest: Jun 05 2026 at 10:22)
• [isabelle] CALL FOR NOMINATION - FSCD Steering Committee ... (4 messages, latest: Jun 05 2026 at 09:42)
• [isabelle] New in the AFP: Type Annotations with Roundtri... (1 message, latest: Jun 04 2026 at 11:29)
• [isabelle] (BUG) Interaction of 'a sort with axiomatic ty... (1 message, latest: Jun 04 2026 at 11:21)
• [isabelle] NEW: IsabelleBlueprint (1 message, latest: Jun 01 2026 at 18:21)
• [isabelle] New in the AFP: The Gelfand–Naimark–Segal Cons... (1 message, latest: Jun 01 2026 at 16:04)
• [isabelle] New in the AFP: Busy Beaver Function (1 message, latest: Jun 01 2026 at 14:14)
• [isabelle] PERR 2026 @ CAV/FLOC: Call for Participation (1 message, latest: Jun 01 2026 at 09:18)
• [isabelle] WPTE 2026 - Call for Participation - Rewriting... (1 message, latest: May 29 2026 at 21:10)
• [isabelle] New in the AFP: Erdős-Ginzburg-Ziv (1 message, latest: May 29 2026 at 16:02)
• [isabelle] Call for participation - FLoC'26 workshop Trib... (1 message, latest: May 29 2026 at 10:06)
• [isabelle] New in the AFP: Seifert–van Kampen Theorem (1 message, latest: May 28 2026 at 15:53)
• [isabelle] TyDe 2026: Second call for papers (1 message, latest: May 28 2026 at 13:26)
• [isabelle] difficulties with "value" (6 messages, latest: May 28 2026 at 09:04)
• [isabelle] List update pattern xs[i := f(xs!i) (10 messages, latest: May 27 2026 at 08:14)
• [isabelle] PDF hyperlinking for @{thm[source]} and friends (1 message, latest: May 23 2026 at 00:22)
• [isabelle] complete_linear_order implementation for HOL-L... (1 message, latest: May 22 2026 at 15:14)
• [isabelle] International School on Rewriting -- 12 to 16 ... (1 message, latest: May 21 2026 at 14:58)
• [isabelle] 2nd CFP - Express/SOS 2026 (@CONFEST) (1 message, latest: May 21 2026 at 08:14)
• [isabelle] Accessing definitions in a locale from outside (2 messages, latest: May 18 2026 at 07:16)
• [isabelle] Last CfP: Autumn School: Proof and Computation... (1 message, latest: May 15 2026 at 08:21)
• [isabelle] Available AI tools (3 messages, latest: May 13 2026 at 15:49)
• [isabelle] TyDe 2026: 1st Call for Papers (1 message, latest: May 13 2026 at 14:58)
• [isabelle] New in the AFP: Mostowski Collapse (1 message, latest: May 13 2026 at 14:55)
• [isabelle] New in the AFP: Andrew's Monotone Chain Convex... (1 message, latest: May 12 2026 at 09:47)
• [isabelle] New in the AFP: Alon’s Combinatorial Nullstell... (1 message, latest: May 10 2026 at 14:49)
• [isabelle] New in the AFP: Nash Equilibria for Finite Games (1 message, latest: May 08 2026 at 17:54)
• [isabelle] New in the AFP: Aho-Corasick String Matching (1 message, latest: May 06 2026 at 16:07)
• [isabelle] Help wanted figuring out peculiar/somewhat bro... (1 message, latest: May 06 2026 at 14:39)
• [isabelle] AITP 2026 FINAL CALL FOR CONTRIBUTIONS - EXTEN... (1 message, latest: May 05 2026 at 13:11)
• [isabelle] Set difference syntax change? (16 messages, latest: May 04 2026 at 19:21)
• [isabelle] SC-Square: Second deadline extension (1 message, latest: May 04 2026 at 15:04)
• [isabelle] UK internship AWS Automated Reasoning Group (1 message, latest: May 04 2026 at 11:22)
• [isabelle] Deadline Ext. 7.5: ThEdu'26 at FLoC, Lisbon (1 message, latest: May 01 2026 at 06:44)
• [isabelle] New in the AFP: Nagata Factoriality (1 message, latest: Apr 30 2026 at 18:07)
• [isabelle] RC 2026: Call for Participation (1 message, latest: Apr 29 2026 at 17:18)
• [isabelle] Request to distribute: CFP: 1st International ... (1 message, latest: Apr 29 2026 at 06:21)
• [isabelle] Managing heap-images of different versions of ... (3 messages, latest: Apr 28 2026 at 11:05)
• [isabelle] Third CfP: Festschrift and Workshop in Honor o... (1 message, latest: Apr 27 2026 at 13:03)
• [isabelle] Call for papers: Isabelle Workshop 2026 (FLoC ... (3 messages, latest: Apr 27 2026 at 09:43)
• [isabelle] New in the AFP: Archimedes' Cattle Problem (1 message, latest: Apr 26 2026 at 14:13)
• [isabelle] New in the AFP: Nominal Unification (1 message, latest: Apr 24 2026 at 19:35)
• [isabelle] Deadline Extension: PERR2026 @ CAV/FLOC (1 message, latest: Apr 24 2026 at 12:08)
• [isabelle] International Workshop on Confluence (IWC) - F... (2 messages, latest: Apr 24 2026 at 10:38)
• [isabelle] WPTE 2026: Second Call for Papers (1 message, latest: Apr 22 2026 at 15:19)
• [isabelle] LAST Cfp ThEdu'26 at FLoC, Lisbon (1 message, latest: Apr 21 2026 at 09:49)
• [isabelle] On verification of predecessor query operations (1 message, latest: Apr 20 2026 at 20:52)
• [isabelle] Job announcement (2 messages, latest: Apr 20 2026 at 18:03)
• [isabelle] Tenth Working Formal Methods Symposium (FROM 2... (1 message, latest: Apr 20 2026 at 17:38)
• [isabelle] 2nd CfP: Autumn School: Proof and Computation ... (1 message, latest: Apr 20 2026 at 12:42)
• [isabelle] PERR2026 @ CAV/FLOC: Second Call For Papers (1 message, latest: Apr 15 2026 at 10:21)
• [isabelle] [ISSUE] PIDE reports wrong error line and mess... (4 messages, latest: Apr 13 2026 at 21:36)
• [isabelle] SC-Square 2026: Deadline Extension (1 message, latest: Apr 13 2026 at 16:59)
• [isabelle] 2nd CfP: LFMTP 2026 - Logical Frameworks and M... (1 message, latest: Apr 13 2026 at 12:07)
• [isabelle] Sledgehammer exports TPTP reserved keywords as... (4 messages, latest: Apr 10 2026 at 08:41)
• [isabelle] New in the AFP: Abstract Consistency Properties (1 message, latest: Apr 09 2026 at 09:56)
• [isabelle] finite maps and lifting (16 messages, latest: Apr 08 2026 at 13:45)
• [isabelle] FLoC'26 workshop - Tribute to Gilles Dowek - C... (1 message, latest: Apr 07 2026 at 05:22)
• [isabelle] New in the AFP: SAT is Not Solvable in Constan... (1 message, latest: Apr 04 2026 at 17:01)
• [isabelle] VSCode LSP: Bad JSON value in Dynamic_Output (... (1 message, latest: Apr 04 2026 at 10:40)
• [isabelle] FMICS 2026: Last Call for Papers! (2 messages, latest: Apr 03 2026 at 01:14)
• [isabelle] Deadline Extenstion: 19th Conference on Intell... (1 message, latest: Mar 31 2026 at 14:05)
• [isabelle] FSCD 2028: Call for Location (1 message, latest: Mar 30 2026 at 15:50)
• [isabelle] Call for Papers: Foundations of Computer Security (1 message, latest: Mar 27 2026 at 16:27)
• [isabelle] [3rd CFP] SCML-2026 International Conference o... (1 message, latest: Mar 27 2026 at 12:06)
• [isabelle] ICE 2026: Second Call for Papers (1 message, latest: Mar 24 2026 at 19:19)
• [isabelle] SC-Square 2026: Second Call for Papers (1 message, latest: Mar 24 2026 at 18:19)
• [isabelle] Advancing AI for Mathematics: Grant Opportunity (1 message, latest: Mar 24 2026 at 18:13)
• [isabelle] Isabelle/REPL (9 messages, latest: Mar 24 2026 at 09:26)
• [isabelle] CFP: WADT 2026 (1 message, latest: Mar 23 2026 at 13:40)
• [isabelle] New in the AFP: Sorted Rewriting by Akihisa Ya... (1 message, latest: Mar 22 2026 at 19:39)
• [isabelle] Simplifier fails when dealing with mix of Pure... (5 messages, latest: Mar 21 2026 at 09:35)
• [isabelle] AI for Math Summer Fellowship -- Copilots for ... (1 message, latest: Mar 21 2026 at 02:10)
• [isabelle] New in the AFP: Lebesgue-Stieltjes Integral (1 message, latest: Mar 20 2026 at 17:00)
• [isabelle] Copilot (or other programming assistants) for ... (35 messages, latest: Mar 19 2026 at 18:22)
• [isabelle] New in the AFP: Isabelle/Solidity (1 message, latest: Mar 17 2026 at 17:56)
• [isabelle] New in the AFP: Formal Verification of Axiom-F... (1 message, latest: Mar 17 2026 at 13:25)
• [isabelle] 2nd CfP: 19th Conference on Intelligent Comput... (1 message, latest: Mar 16 2026 at 14:00)
• [isabelle] WPTE 2026: Call for Papers (1 message, latest: Mar 15 2026 at 21:52)
• [isabelle] Introducing AutoReal: A Cost-Efficient Local L... (1 message, latest: Mar 15 2026 at 12:42)
• [isabelle] Marktoberdorf Summer School 2026: Call for Par... (1 message, latest: Mar 13 2026 at 22:22)
• [isabelle] ATP Problem Encoding Issue (6 messages, latest: Mar 10 2026 at 18:14)
• [isabelle] Second CfP: Festschrift and Workshop in Honor ... (1 message, latest: Mar 10 2026 at 17:22)
• [isabelle] PhD Position in Bridging the Gap Between Mathe... (1 message, latest: Mar 10 2026 at 09:57)
• [isabelle] Call for Participation: Workshop on AI and The... (1 message, latest: Mar 10 2026 at 05:03)
• [isabelle] AITP 2026 - Call for Contributions (1 message, latest: Mar 09 2026 at 10:12)
• [isabelle] VSTTE 2026: First Call for Papers and WIP Pres... (1 message, latest: Mar 08 2026 at 15:18)
• [isabelle] Claude/Copilot (or other programming assistant... (2 messages, latest: Mar 05 2026 at 15:27)
• [isabelle] LFMTP 2026 -- Call for papers (1 message, latest: Mar 04 2026 at 10:47)
• [isabelle] Cfp ThEdu'26 , 19 July 2026, Lisbon, Portugal (1 message, latest: Mar 03 2026 at 18:23)
• [isabelle] Immediate theorem dependencies (like thm_deps)... (3 messages, latest: Mar 02 2026 at 11:46)
• [isabelle] Major/minor versioning discipline for Isabelle... (9 messages, latest: Feb 27 2026 at 06:55)
• [isabelle] RExAI Call for Papers (1 message, latest: Feb 26 2026 at 11:59)
• [isabelle] CfP: CI-BD-SOQE 2026: Workshop on Craig Interp... (1 message, latest: Feb 25 2026 at 13:35)
• [isabelle] Call for Participation: Functional and Logic P... (1 message, latest: Feb 25 2026 at 13:35)
• [isabelle] UNSOUND Workshop at ECOOP 2026 (1 message, latest: Feb 24 2026 at 21:31)
• [isabelle] International Workshop on Confluence (IWC) - 2... (1 message, latest: Feb 23 2026 at 09:22)
• [isabelle] Announcing Isabelle/Copilot, an AI-driven assi... (6 messages, latest: Feb 20 2026 at 10:22)
• [isabelle] ICE 2026: First Call for Papers (1 message, latest: Feb 19 2026 at 18:26)
• [isabelle] PhD on the Verification of Statistical Model C... (1 message, latest: Feb 19 2026 at 14:30)
• [isabelle] Interactive Isabelle session with remote prover (2 messages, latest: Feb 18 2026 at 12:33)
• [isabelle] FTfJP CfP, deadline extended (1 message, latest: Feb 17 2026 at 11:32)
• [isabelle] polarity of recursive unbundling (1 message, latest: Feb 17 2026 at 11:31)
• [isabelle] CfP: 19th Conference on Intelligent Computer M... (1 message, latest: Feb 16 2026 at 18:05)
• [isabelle] Autumn school "Proof and Computation", Fischba... (1 message, latest: Feb 15 2026 at 15:56)
• [isabelle] Automating Mathematical Reasoning: Interaction... (2 messages, latest: Feb 15 2026 at 11:01)
• [isabelle] Possible bug in Nitpick — finds counterexample... (1 message, latest: Feb 15 2026 at 11:01)
• [isabelle] Talk Invitaiton: Unsoundness in Isabelle subla... (3 messages, latest: Feb 12 2026 at 19:28)
• [isabelle] TYPES 2026: Call for Participation (1 message, latest: Feb 12 2026 at 09:56)
• [isabelle] [2nd CFP] SCML-2026 International Conference o... (1 message, latest: Feb 11 2026 at 21:33)
• [isabelle] TCS special issue on Universality in Logics an... (1 message, latest: Feb 11 2026 at 15:36)
• [isabelle] [CFP] AIPV 2026: AI, Proof and Verification (F... (1 message, latest: Feb 11 2026 at 02:07)
• [isabelle] New in the AFP: Workflow Net Fitness Measures ... (1 message, latest: Feb 09 2026 at 13:15)
• [isabelle] CS Teaching Fellow, Lancaster Leipzig (1 message, latest: Feb 09 2026 at 10:48)
• [isabelle] Isabelle/jEdit becomes unstable after sledgeha... (3 messages, latest: Feb 08 2026 at 05:42)
• [isabelle] SC-Square 2026: First Call for Papers (1 message, latest: Feb 05 2026 at 17:12)
• [isabelle] New in the AFP: Two HOL-CSP related entries. (1 message, latest: Feb 03 2026 at 18:31)
• [isabelle] New in the AFP: 'Sets' Revisited: Working with... (1 message, latest: Feb 03 2026 at 15:36)
• [isabelle] New in the AFP: Concentrated Liquidity Market ... (1 message, latest: Feb 03 2026 at 15:20)
• [isabelle] New in the AFP: Arbitrage Opportunities Corres... (1 message, latest: Feb 03 2026 at 15:00)
• [isabelle] AFP down (5 messages, latest: Feb 02 2026 at 10:27)
• [isabelle] Alignment of super- and subscripts in generate... (4 messages, latest: Jan 31 2026 at 19:30)
• [isabelle] Preprint on grounded arithmetic (GA) metatheor... (14 messages, latest: Jan 31 2026 at 16:19)
• [isabelle] Removing a rule from the intro! set (2 messages, latest: Jan 31 2026 at 11:09)
• [isabelle] CMCS 2026: Second Call for Papers and Deadline... (1 message, latest: Jan 29 2026 at 22:11)
• [isabelle] fun package raises exceptions on the following... (1 message, latest: Jan 29 2026 at 12:20)
• [isabelle] Isabelle 2025-2 crash report (12 messages, latest: Jan 28 2026 at 12:11)
• [isabelle] pdflatex as an isabelle tool (2 messages, latest: Jan 27 2026 at 18:47)
• [isabelle] ITP 2027 - Call for Bids (1 message, latest: Jan 27 2026 at 18:14)
• [isabelle] 2nd International Conference on Artificial Int... (1 message, latest: Jan 27 2026 at 16:21)
• [isabelle] Ignored {} sort constraint when using undersco... (3 messages, latest: Jan 27 2026 at 10:54)
• [isabelle] NEU: Festschrift and Workshop in Honor of Davi... (1 message, latest: Jan 26 2026 at 16:28)
• [isabelle] LSFA 2026 Announcement and First Call for Papers (1 message, latest: Jan 25 2026 at 17:19)
• [isabelle] New in the AFP: Swap Distance / Linear orders ... (1 message, latest: Jan 25 2026 at 15:45)
• [isabelle] New in the AFP: Abel's Limit Theorem (1 message, latest: Jan 23 2026 at 15:21)
• [isabelle] Low level simplifier failure (7 messages, latest: Jan 22 2026 at 10:03)
• [isabelle] 2nd CfP: REVERSIBLE COMPUTATION 2026 –18th Int... (1 message, latest: Jan 21 2026 at 15:49)
• [isabelle] Announcing Isabelle2025-2 (1 message, latest: Jan 20 2026 at 09:52)
• [isabelle] CFP --- International Conference on Graph Tran... (1 message, latest: Jan 19 2026 at 22:22)
• [isabelle] Rogue poly-process at 100% CPU without jedit d... (4 messages, latest: Jan 19 2026 at 22:09)
• [isabelle] FTfJP 2026 at ECOOP Call for Papers (1 message, latest: Jan 19 2026 at 22:09)
• [isabelle] Post-doc position at Inria Rennes on AI and fo... (1 message, latest: Jan 19 2026 at 16:36)
• [isabelle] Isabelle build alaways accepts `sorry` (4 messages, latest: Jan 17 2026 at 19:59)
• [isabelle] New in the AFP: Compressed Oracles (1 message, latest: Jan 16 2026 at 16:22)
• [isabelle] Call For Papers: 6th Workshop on Program Equiv... (1 message, latest: Jan 15 2026 at 14:23)
• [isabelle] FTfJP 2026 call for papers (1 message, latest: Jan 13 2026 at 18:17)
• [isabelle] International Workshop on Confluence 1st CfP (1 message, latest: Jan 13 2026 at 11:35)
• [isabelle] Does Isabelle/VSCode support remote SSH? (2 messages, latest: Jan 12 2026 at 19:13)
• [isabelle] TYPES 2026: Deadline Extension and Final Call ... (1 message, latest: Jan 11 2026 at 11:59)
• [isabelle] Trouble Installing Isabelle2025-1 under Windows (2 messages, latest: Jan 10 2026 at 14:27)
• [isabelle] FSCD 2026: Second Call for Papers (1 message, latest: Jan 09 2026 at 15:41)
• [isabelle] CMCS 2026: Call for Papers (1 message, latest: Jan 08 2026 at 14:53)
• [isabelle] ITP'26:  Second Call for Papers (1 message, latest: Jan 07 2026 at 13:44)
• [isabelle] (Call for Participation) Dafny Workshop at POP... (2 messages, latest: Jan 06 2026 at 12:31)
• [isabelle] ML_IDENTIFIER (2 messages, latest: Jan 02 2026 at 21:06)
• [isabelle] Forced line breaks in mixfix annotations (1 message, latest: Jan 02 2026 at 20:20)
• [isabelle] FMICS: Call for Papers (1 message, latest: Dec 31 2025 at 02:14)
• [isabelle] New in the AFP: Set Reconciliation (1 message, latest: Dec 27 2025 at 17:22)
• [isabelle] New in the AFP: Dynamic Pushdown Networks (1 message, latest: Dec 24 2025 at 15:36)
• [isabelle] [TFP 2026] 1st Call for Participation for the ... (1 message, latest: Dec 24 2025 at 15:33)
• [isabelle] VerifyThis26: Call for problems (1 message, latest: Dec 23 2025 at 12:39)
• [isabelle] PDF documents missing on the AFP website (7 messages, latest: Dec 22 2025 at 06:31)
• [isabelle] AFP 2025-1 mismatch (3 messages, latest: Dec 20 2025 at 22:06)
• [isabelle] AFP 2025-1 (1 message, latest: Dec 20 2025 at 00:56)
• [isabelle] FMBC 2026 - Second Call for Papers (1 message, latest: Dec 19 2025 at 15:25)
• [isabelle] Simp rules with reducible lhss in Transcendent... (6 messages, latest: Dec 19 2025 at 14:46)
• [isabelle] Announcing Isabelle2025-1 (3 messages, latest: Dec 18 2025 at 11:21)
• [isabelle] ThEdu'25 Post Proceedings - Call for Papers (1 message, latest: Dec 16 2025 at 18:06)
• [isabelle] Associate/Assistant professorships in Copenhag... (1 message, latest: Dec 15 2025 at 16:11)
• [isabelle] CfP: SCML-2026 - International Conference on S... (1 message, latest: Dec 15 2025 at 10:32)
• [isabelle] Isabelle2025-1-RC4: isabelle process_theories ... (1 message, latest: Dec 10 2025 at 22:27)
• [isabelle] Post Doc position at University of North Carol... (1 message, latest: Dec 09 2025 at 23:38)
• [isabelle] Nitro Isolation Engine: a formally verified hy... (2 messages, latest: Dec 09 2025 at 16:23)
• [isabelle] Isabelle2025-1-RC4: state of Isabelle/VSCode (2 messages, latest: Dec 09 2025 at 10:04)
• [isabelle] Left-open bundle in Leftist_Heap causing problems (2 messages, latest: Dec 09 2025 at 09:25)
• [isabelle] Isabelle2025-1-RC4 available for even more tes... (2 messages, latest: Dec 08 2025 at 22:58)
• [isabelle] Job offer at AWS, asking for experience with p... (2 messages, latest: Dec 07 2025 at 22:38)
• [isabelle] YouTube video on the separation kernel verific... (1 message, latest: Dec 07 2025 at 15:18)
• [isabelle] Big news from Amazon Web Services (1 message, latest: Dec 04 2025 at 19:16)
• [isabelle] Isabelle2025-RC1-1 issues with mouse usage on Mac (4 messages, latest: Dec 04 2025 at 16:35)
• [isabelle] Unofficial fix to the LaTeX generation of Code... (2 messages, latest: Dec 03 2025 at 12:17)
• [isabelle] Isabelle2025-RC3 nondeterministic behaviour wh... (1 message, latest: Dec 03 2025 at 08:28)
• [isabelle] fork for AFP 2025-1 on Mon (2 messages, latest: Dec 03 2025 at 04:40)
• [isabelle] Final CfP: Functional and Logic Programming (F... (1 message, latest: Dec 02 2025 at 18:10)
• [isabelle] Isabelle2025-1-RC2 selecting from Theories pan... (3 messages, latest: Dec 01 2025 at 17:45)
• [isabelle] [Isabelle2025-1-RC1] About try0 (9 messages, latest: Dec 01 2025 at 17:29)
• [isabelle] Isabelle2025-1-RC3 available for final testing... (1 message, latest: Dec 01 2025 at 15:48)
• [isabelle] PhD position at University of New South Wales ... (1 message, latest: Nov 30 2025 at 15:59)
• [isabelle] DisCoTec 2026 - Preliminary Call for Papers (1 message, latest: Nov 27 2025 at 17:16)
• [isabelle] Isar reference manual (3 messages, latest: Nov 27 2025 at 11:03)
• [isabelle] Jonathan Bowen to give the Peter Landin Semant... (1 message, latest: Nov 26 2025 at 02:45)
• [isabelle] New in the AFP: The Weak Spectroscopy Game to ... (1 message, latest: Nov 22 2025 at 09:28)
• [isabelle] New in the AFP: Rely-Guarantee Extensions and ... (1 message, latest: Nov 21 2025 at 15:47)
• [isabelle] ECOOP 2026: Call for AEC members (1 message, latest: Nov 21 2025 at 14:05)
• [isabelle] Isabelle2025-1-RC2 bulky app, notably on macOS (5 messages, latest: Nov 20 2025 at 11:33)
• [isabelle] [Isabelle2025-1-RC2] About try0 (4 messages, latest: Nov 20 2025 at 06:50)
• [isabelle] Isabelle2025-1-RC2 available for further testi... (1 message, latest: Nov 19 2025 at 19:46)
• [isabelle] FMBC26 - First Call for Papers (1 message, latest: Nov 19 2025 at 12:33)
• [isabelle] [Isabelle2025-1-RC1] Porting Isabelle_LLVM (12 messages, latest: Nov 19 2025 at 10:12)
• [isabelle] Isabelle 2025-1, RC-1: Problems with Code-Equa... (2 messages, latest: Nov 19 2025 at 07:43)
• [isabelle] New in the AFP: Pre*: The Predecessors of a Re... (1 message, latest: Nov 18 2025 at 14:22)
• [isabelle] Isabelle 2025 import issues (3 messages, latest: Nov 18 2025 at 04:34)
• [isabelle] New in the AFP: Formalizing Neural Networks by... (1 message, latest: Nov 17 2025 at 12:52)
• [isabelle] CfP: REVERSIBLE COMPUTATION 2026 –18th Interna... (1 message, latest: Nov 14 2025 at 14:08)
• [isabelle] Multiple Postdoc and PhD positions in Melbourne (1 message, latest: Nov 14 2025 at 03:30)
• [isabelle] Pretty-printing terms without syntactic sugar (4 messages, latest: Nov 13 2025 at 12:18)
• [isabelle] 4 PhD positions in Automated Reasoning at TU W... (1 message, latest: Nov 13 2025 at 08:57)
• [isabelle] Ctrl+click on notation with sub- and superscri... (1 message, latest: Nov 13 2025 at 08:38)
• [isabelle] Call for Papers: Tests and Proofs (TAP) (Now a... (3 messages, latest: Nov 12 2025 at 18:24)
• [isabelle] ITP 2026: Call for Papers (1 message, latest: Nov 12 2025 at 14:03)
• [isabelle] FM 2026: Final Call for Papers (1 message, latest: Nov 10 2025 at 11:37)
• [isabelle] Isabelle2025-RC1-1 selecting from Theories pan... (1 message, latest: Nov 07 2025 at 17:13)
• [isabelle] Isabelle2025-RC1-1 available for testing (2 messages, latest: Nov 07 2025 at 10:54)
• [isabelle] FSCD 2026: First Call for Papers (1 message, latest: Nov 06 2025 at 17:39)
• [isabelle] Isabelle2025-1_RC0 code generation regression (7 messages, latest: Nov 03 2025 at 18:01)
• [isabelle] LMS Computer Science Colloquium 2025: Combinat... (1 message, latest: Nov 03 2025 at 02:44)
• [isabelle] Jeremy Avigad to give this year's LMS/BCS-FACS... (3 messages, latest: Nov 03 2025 at 01:59)
• [isabelle] prefix and postfix type syntax printing (1 message, latest: Oct 31 2025 at 12:03)
• [isabelle] [TFP 2026] 2nd Call for Papers for the 27th In... (1 message, latest: Oct 30 2025 at 09:34)
• [isabelle] New in the AFP: Path Equivalence and Automatio... (1 message, latest: Oct 25 2025 at 11:49)
• [isabelle] cl-isabelle-users Digest Fri, 24 Oct 2025 (1/1) (1 message, latest: Oct 24 2025 at 20:21)
• [isabelle] Theorems about theorems (5 messages, latest: Oct 24 2025 at 11:09)
• [isabelle] 2nd CfP: Functional and Logic Programming (FLO... (1 message, latest: Oct 23 2025 at 13:49)
• [isabelle] TYPES 2026 Call for Contributions (1 message, latest: Oct 21 2025 at 17:42)
• [isabelle] Functional Data Structures and Algorithms: A P... (1 message, latest: Oct 20 2025 at 23:49)
• [isabelle] New in the AFP: Muntac: A Verified Certificate... (1 message, latest: Oct 20 2025 at 16:45)
• [isabelle] cl-isabelle-users Digest Sun, 19 Oct 2025 (1/1) (1 message, latest: Oct 20 2025 at 07:41)
• [isabelle] Question on Cycle dependency error when export... (5 messages, latest: Oct 20 2025 at 01:23)
• [isabelle] New in the AFP: Pushdown Automata (1 message, latest: Oct 17 2025 at 18:55)
• [isabelle] New in the AFP: Z Mathematical Toolkit in Isab... (1 message, latest: Oct 17 2025 at 11:45)
• [isabelle] Isabelle2025-1-RC0 available for experimentation (1 message, latest: Oct 13 2025 at 13:15)
• [isabelle] Conflicting name spaces (3 messages, latest: Oct 13 2025 at 11:29)
• [isabelle] ANU 33rd Logic Summer School, 1–12 December 2025 (1 message, latest: Oct 13 2025 at 03:39)
• [isabelle] New in the AFP: Relational Divisibility (1 message, latest: Oct 10 2025 at 11:39)
• [isabelle] cl-isabelle-users Digest Fri, 10 Oct 2025 (1/1) (1 message, latest: Oct 10 2025 at 03:45)
• [isabelle] syntax highlighting for type variables (2 messages, latest: Oct 09 2025 at 09:16)
• [isabelle] Special Issue on Horn Clauses for Verification... (1 message, latest: Oct 04 2025 at 08:40)
• [isabelle] (3rd CfP) Dafny Workshop at POPL 2026 (1 message, latest: Oct 02 2025 at 14:44)
• [isabelle] cl-isabelle-users Digest Wed, 01 Oct 2025 (1/1) (1 message, latest: Oct 01 2025 at 04:26)
• [isabelle] RSSRail 2025: CfPart (Reliability, Safety, and... (1 message, latest: Sep 30 2025 at 12:19)
• [isabelle] e-graphs and equational theories (1 message, latest: Sep 23 2025 at 19:42)
• [isabelle] Feedback on Isabelle environment, especially d... (1 message, latest: Sep 23 2025 at 13:47)
• [isabelle] cl-isabelle-users Digest Tue, 23 Sep 2025 (1/1) (1 message, latest: Sep 23 2025 at 05:23)
• [isabelle] [TFP 2026] Call for Papers for the 27th Intern... (1 message, latest: Sep 22 2025 at 08:24)
• [isabelle] Kick-off meeting of the Malinca ERC Synergy Pr... (1 message, latest: Sep 17 2025 at 09:35)
• [isabelle] locale lemmas introspection (1 message, latest: Sep 15 2025 at 13:22)
• [isabelle] New in the AFP: Greibach Normal Form (2 messages, latest: Sep 13 2025 at 08:27)
• [isabelle] New in the AFP: Stratified Datalog and Program... (2 messages, latest: Sep 13 2025 at 07:56)
• [isabelle] FM 2026: 2nd Call for Papers (1 message, latest: Sep 12 2025 at 10:06)
• [isabelle] Automated theorem proving in generalized algeb... (2 messages, latest: Sep 09 2025 at 13:47)
• [isabelle] (2nd CfP) Dafny Workshop at POPL 2026 (1 message, latest: Sep 09 2025 at 13:08)
• [isabelle] Executing set comprehensions (6 messages, latest: Sep 05 2025 at 13:18)
• [isabelle] New in the AFP: No-free-lunch theorem for mach... (1 message, latest: Sep 01 2025 at 20:28)
• [isabelle] S-REPLS (Amazon, 29 Oct) - Call for talks and ... (1 message, latest: Aug 29 2025 at 09:49)
• [isabelle] Call for Abstracts: Workshop on Natural Formal... (1 message, latest: Aug 26 2025 at 06:23)
• [isabelle] CfP: Symposium on Functional and Logic Program... (1 message, latest: Aug 25 2025 at 13:57)
• [isabelle] I/Q plugin for AI <-> Isabelle/jEdit interaction (1 message, latest: Aug 22 2025 at 12:44)
• [isabelle] (CfP) Dafny Workshop at POPL 2026 (1 message, latest: Aug 20 2025 at 10:55)
• [isabelle] PSSL111 - Second Announcement (1 message, latest: Aug 18 2025 at 13:28)
• [isabelle] slow "text" in HOL-Analysis.Infinite_Sum (5 messages, latest: Aug 16 2025 at 17:49)
• [isabelle] Unexpected printing of nested PROP functions (7 messages, latest: Aug 15 2025 at 21:36)
• [isabelle] Sound theorem instantiation rejected in Pure/g... (8 messages, latest: Aug 15 2025 at 11:30)
• [isabelle] New in the AFP: Mission-time Linear Temporal L... (2 messages, latest: Aug 14 2025 at 10:36)
• [isabelle] subsequence pre-order on lazy lists (5 messages, latest: Aug 13 2025 at 16:19)
• [isabelle] very slow metis proofs: is that an issue? (9 messages, latest: Aug 13 2025 at 09:43)
• [isabelle] Getting rid of abbreviation from imported theory? (1 message, latest: Aug 13 2025 at 07:42)
• [isabelle] FroCoS/ITP/TABLEAUX 2025 call for participation (1 message, latest: Aug 11 2025 at 16:01)
• [isabelle] New in the AFP: Two-Way Deterministic Finite A... (1 message, latest: Aug 08 2025 at 14:18)
• [isabelle] Performance of AFP/Padic_Fields (3 messages, latest: Aug 07 2025 at 17:23)
• [isabelle] Program Synthesis libraries or projects? (2 messages, latest: Aug 07 2025 at 11:45)
• [isabelle] POPL 2026 Call For Tutorials (1 message, latest: Aug 06 2025 at 18:13)
• [isabelle] FMCAD 2025 - Call for Participation (1 message, latest: Aug 06 2025 at 06:27)
• [isabelle] Redundant facts (inj_on_subset/subset_inj_on) ... (2 messages, latest: Aug 03 2025 at 16:29)
• [isabelle] cl-isabelle-users Digest Sat, 02 Aug 2025 (1/1) (1 message, latest: Aug 02 2025 at 04:05)
• [isabelle] Another little AI experiment (1 message, latest: Aug 01 2025 at 14:57)
• [isabelle] New in the AFP: Unconstrained Optimization (1 message, latest: Aug 01 2025 at 10:58)
• [isabelle] [CFP] ALIGN 2025 – Workshop on Alignments and ... (1 message, latest: Jul 31 2025 at 19:27)
• [isabelle] "Duplicate use of directory in session" error (4 messages, latest: Jul 30 2025 at 09:11)
• [isabelle] New in the AFP: Universal Pairs for Diophantin... (1 message, latest: Jul 29 2025 at 18:36)
• [isabelle] DeepSeek experiment (7 messages, latest: Jul 28 2025 at 09:55)
• [isabelle] AFP, AutoCorres2, write permission (2 messages, latest: Jul 27 2025 at 22:48)
• [isabelle] New in the AFP: A meta-modal logic for bisimul... (1 message, latest: Jul 24 2025 at 21:57)
• [isabelle] Merging elimination rules of Claset is slow - ... (36 messages, latest: Jul 21 2025 at 16:03)
• [isabelle] New in the AFP: Löb's theorem (1 message, latest: Jul 18 2025 at 14:40)
• [isabelle] Datatype definition efficiency - workaround fo... (1 message, latest: Jul 17 2025 at 23:36)
• [isabelle] Nineteenth International Tbilisi Summer School... (1 message, latest: Jul 15 2025 at 07:55)
• [isabelle] Deriving logic programs from equational theories (2 messages, latest: Jul 15 2025 at 07:40)
• [isabelle] First Workshop on Logic Statistical and Neural... (1 message, latest: Jul 15 2025 at 02:25)
• [isabelle] Gemini 2.5 Pro AI vs ω-categories and schemes ... (1 message, latest: Jul 14 2025 at 12:48)
• [isabelle] Symbolic Computation and Machine Learning (Cal... (1 message, latest: Jul 11 2025 at 20:56)
• [isabelle] Datatype definition efficiency (9 messages, latest: Jul 11 2025 at 17:43)
• [isabelle] FSCD 2025: Free online participation, 15 - 18 ... (1 message, latest: Jul 09 2025 at 20:33)
• [isabelle] Archive of formal problems? (2 messages, latest: Jul 08 2025 at 11:21)
• [isabelle] DataMod 2025 - First Call for Papers (3 messages, latest: Jul 07 2025 at 13:39)
• [isabelle] beginners eisbach issues (1 message, latest: Jul 07 2025 at 12:54)
• [isabelle] New in the AFP: The Oneway to Hiding Theorem (1 message, latest: Jul 07 2025 at 11:07)
• [isabelle] New in the AFP: Kraus Maps (1 message, latest: Jul 07 2025 at 10:04)
• [isabelle] New in the AFP: Parikh's theorem (1 message, latest: Jul 07 2025 at 09:32)
• [isabelle] New in the AFP: Computational p-Adics (1 message, latest: Jul 07 2025 at 08:15)
• [isabelle] POPL 2026 Last Call for Papers (1 message, latest: Jul 05 2025 at 02:12)
• [isabelle] FYI: kernel :: ('a => 'b) => ('a * 'a) set (1 message, latest: Jul 03 2025 at 14:19)
• [isabelle] Merging theory definitions calls normalise too... (4 messages, latest: Jun 30 2025 at 18:12)
• [isabelle] CFP: Special Issue on “Bridging Formal Verific... (1 message, latest: Jun 27 2025 at 10:30)
• [isabelle] extended deadline (6th July): Autumn school "P... (1 message, latest: Jun 27 2025 at 10:30)
• [isabelle] New in the AFP: The Hidden Number Problem (1 message, latest: Jun 26 2025 at 13:32)
• [isabelle] New in the AFP: A Modular Splitting Framework ... (1 message, latest: Jun 26 2025 at 13:29)
• [isabelle] New in the AFP: The Sigmoid Function and the U... (1 message, latest: Jun 26 2025 at 13:27)
• [isabelle] Question regarding lifting/transfer (2 messages, latest: Jun 26 2025 at 05:45)
• [isabelle] Lifting and Code Generator (2 messages, latest: Jun 24 2025 at 16:34)
• [isabelle] POPL 2026 Call for Papers (1 message, latest: Jun 24 2025 at 01:54)
• [isabelle] POPL 2026 Call for Workshops (1 message, latest: Jun 24 2025 at 01:34)
• [isabelle] ML Family Workshop 2025: extended deadline: Ju... (1 message, latest: Jun 21 2025 at 10:12)
• [isabelle] Deadline Extended: CfP ICTAC'2025 (1 message, latest: Jun 20 2025 at 16:15)
• [isabelle] FSCD 2025: Third Call for Participation (late ... (1 message, latest: Jun 19 2025 at 12:23)
• [isabelle] 2 x new in the AFP: Dyck Language / Chomsky-Sc... (1 message, latest: Jun 19 2025 at 10:55)
• [isabelle] VSTTE 2025: Second call for papers (1 message, latest: Jun 18 2025 at 18:59)
• [isabelle] Galois Energy Games (1 message, latest: Jun 17 2025 at 19:47)
• [isabelle] Minus on lists (7 messages, latest: Jun 14 2025 at 13:23)
• [isabelle] sym/trans attributes missing from reference ma... (1 message, latest: Jun 13 2025 at 16:42)
• [isabelle] Meeting IFIP WG 1.6 on Rewriting: Call for Par... (1 message, latest: Jun 13 2025 at 15:10)
• [isabelle] Call for participation to UNIF 2025 (1 message, latest: Jun 12 2025 at 17:06)
• [isabelle] PhD Position in Parametric Floating-Point Reas... (1 message, latest: Jun 11 2025 at 20:06)
• [isabelle] ML Family Workshop 2025: 2nd CFP: deadline Jun... (1 message, latest: Jun 05 2025 at 09:59)
• [isabelle] Sledgehammer vs "hammers" (11 messages, latest: Jun 05 2025 at 09:59)
• [isabelle] FSCD 2025: Second Call for Participation (stud... (1 message, latest: Jun 04 2025 at 22:29)
• [isabelle] New in the AFP: Faithful Logic Embeddings in HOL (1 message, latest: Jun 04 2025 at 14:11)
• [isabelle] New in the AFP: A Verified Reduction Algorithm... (1 message, latest: Jun 04 2025 at 13:38)
• [isabelle] Separating local facts from rules in sledgeham... (4 messages, latest: Jun 04 2025 at 07:52)
• [isabelle] CFP - 1st International Workshop on Logic, Sta... (1 message, latest: Jun 03 2025 at 11:18)
• [isabelle] New in the AFP: Restriction Spaces and applica... (1 message, latest: Jun 02 2025 at 15:54)
• [isabelle] School on Symbolic and Statistical Methods for... (1 message, latest: Jun 02 2025 at 06:33)
• [isabelle] Autumn school "Proof and Computation", Herrsch... (2 messages, latest: May 31 2025 at 12:08)
• [isabelle] CALCO/MFPS 2025: Second Call for Participation (1 message, latest: May 30 2025 at 21:56)
• [isabelle] Monoid or word homomorphism? (4 messages, latest: May 29 2025 at 16:03)
• [isabelle] Issues with `polyc` on macOS (3 messages, latest: May 29 2025 at 07:59)
• [isabelle] New in the AFP: Context-Free Grammars and Lang... (1 message, latest: May 28 2025 at 22:53)
• [isabelle] Session dependency graph? (1 message, latest: May 28 2025 at 18:33)
• [isabelle] ECOOP 2025: Call for Participation - Early Reg... (1 message, latest: May 27 2025 at 07:26)
• [isabelle] blast_trace (1 message, latest: May 26 2025 at 13:20)
• [isabelle] New in the AFP: Shallow Expressions (1 message, latest: May 24 2025 at 18:39)
• [isabelle] New in the AFP: Munta: A Verified Model Checke... (1 message, latest: May 23 2025 at 13:31)
• [isabelle] Isabelle dev blog no longer available? (6 messages, latest: May 22 2025 at 14:03)
• [isabelle] ITP 2025: Call for workshops (1 message, latest: May 22 2025 at 13:53)
• [isabelle] cartouche-based antiquotation syntax for @{thm... (2 messages, latest: May 22 2025 at 13:47)
• [isabelle] [PPDP 25] Extended Call for Papers (1 message, latest: May 22 2025 at 10:39)
• [isabelle] exception Size raised (line 183 of "./basis/Li... (3 messages, latest: May 21 2025 at 14:03)
• [isabelle] Binder syntax for vec_lambda (2 messages, latest: May 21 2025 at 09:15)
• [isabelle] wrong name in Ackermann.thy (5 messages, latest: May 20 2025 at 11:21)
• [isabelle] FSCD 2025: Call for Participation (early regis... (1 message, latest: May 19 2025 at 13:13)
• [isabelle] New in then AFP: Farey Sequences and Ford Circles (1 message, latest: May 18 2025 at 13:31)
• [isabelle] Call for workshops and tutorials associated wi... (1 message, latest: May 14 2025 at 14:46)
• [isabelle] [CFP] SEFM 2025 (1 message, latest: May 14 2025 at 09:26)
• [isabelle] HCVS 2025, **Deadline Extension**: 12th Worksh... (1 message, latest: May 14 2025 at 09:10)
• [isabelle] HOR 2025: Deadline extension - Last Call for P... (1 message, latest: May 14 2025 at 09:10)
• [isabelle] WST 2025 - Workshop on Termination, First Call... (1 message, latest: May 12 2025 at 10:13)
• [isabelle] Suggestion for HOLCF: simproc for continuity s... (3 messages, latest: May 12 2025 at 07:26)
• [isabelle] UNIF 2025: Extended submission deadline (May 17) (1 message, latest: May 10 2025 at 22:02)
• [isabelle] CALCO/MFPS 2025: Call for Participation (1 message, latest: May 09 2025 at 09:30)
• [isabelle] 1st International School on Logical Frameworks... (2 messages, latest: May 07 2025 at 21:22)
• [isabelle] LSFA 2025: Extended Deadlines (abstracts: May ... (1 message, latest: May 07 2025 at 21:16)
• [isabelle] CICM 2025 *** DEADLINES FOR FORMAL SUBMISSIONS... (1 message, latest: May 06 2025 at 10:52)
• [isabelle] Selector value with the value command (8 messages, latest: May 06 2025 at 07:23)
• [isabelle] AITP 2025 FINAL CALL FOR CONTRIBUTIONS - EXTEN... (1 message, latest: May 05 2025 at 21:59)
• [isabelle] New in the AFP: Sophie Germain's Theorem (1 message, latest: May 05 2025 at 11:36)
• [isabelle] 1st Call for Papers Express/SOS 2025 (1 message, latest: May 05 2025 at 10:34)
• [isabelle] About isabelle build's error using afp version... (4 messages, latest: May 04 2025 at 11:12)
• [isabelle] Announcement of Isabelle/DOF 2025 (1 message, latest: May 03 2025 at 12:34)
• [isabelle] HOR 2025: Second Call for Papers (1 message, latest: May 03 2025 at 12:34)
• [isabelle] FTfJP 2025 - 4th Call for Papers (1 message, latest: May 02 2025 at 13:51)
• [isabelle] New in the AFP: Ultrametric Spaces (1 message, latest: May 01 2025 at 14:44)
• [isabelle] integration with LLMs for autocomplete, sugges... (1 message, latest: May 01 2025 at 13:47)
• [isabelle] How to build a base heap containing both HOL-C... (3 messages, latest: May 01 2025 at 13:04)
• [isabelle] UNIF 2025 Last Call for Papers (a FSCD event) (1 message, latest: May 01 2025 at 11:28)
• [isabelle] CICM 2025: 4th Announcement and Call for Paper... (1 message, latest: Apr 25 2025 at 16:02)
• [isabelle] Multiple PhD Positions at the University of Me... (1 message, latest: Apr 25 2025 at 07:04)
• [isabelle] Increase maximum heap size (5 messages, latest: Apr 24 2025 at 16:13)
• [isabelle] HCVS 2025, 2nd CfP: 12th Workshop on Horn Clau... (1 message, latest: Apr 24 2025 at 14:19)
• [isabelle] Finite set computation with the value command (1 message, latest: Apr 24 2025 at 09:18)
• [isabelle] Type inference in "cases" and "induction" method (1 message, latest: Apr 23 2025 at 18:28)
• [isabelle] AutoCorrode (1 message, latest: Apr 23 2025 at 11:21)
• [isabelle] Equality on word literals [was: Word_Lib: Perf... (2 messages, latest: Apr 22 2025 at 23:18)
• [isabelle] LSFA 2025 Last Call for Papers (1 message, latest: Apr 22 2025 at 20:48)
• [isabelle] Marktoberdorf Summer School 2025, August 6-15,... (1 message, latest: Apr 22 2025 at 20:48)
• [isabelle] instance msb :: nat in AutoCorres2 (7 messages, latest: Apr 22 2025 at 17:38)
• [isabelle] Ancient shift bootstrap operations Word_Lib/Si... (1 message, latest: Apr 22 2025 at 17:38)
• [isabelle] Self-container simproc for word numeral normal... (1 message, latest: Apr 22 2025 at 17:36)
• [isabelle] Word theory and shift operations (3 messages, latest: Apr 22 2025 at 17:35)
• [isabelle] try-antiquotation: redundant pattern warning (1 message, latest: Apr 19 2025 at 10:29)
• [isabelle] ML Family Workshop 2025: Call for Presentations (1 message, latest: Apr 19 2025 at 09:21)
• [isabelle] [CHC-COMP 2025] - Call for Solver Submission (1 message, latest: Apr 17 2025 at 08:28)
• [isabelle] Proved False using normalization by evaluation (24 messages, latest: Apr 15 2025 at 16:19)
• [isabelle] FTfJP 2025 - Last CfP (extended deadline) (1 message, latest: Apr 15 2025 at 10:37)
• [isabelle] ACL2-2025 Second Call for Participation (1 message, latest: Apr 15 2025 at 10:37)
• [isabelle] Word_Lib: Performance problem for proving ineq... (3 messages, latest: Apr 15 2025 at 09:05)
• [isabelle] SMT completeness issue: Failure to prove a tru... (7 messages, latest: Apr 14 2025 at 17:46)
• [isabelle] New in the AFP: The Kolmogorov-Chentsov theorem (1 message, latest: Apr 14 2025 at 12:20)
• [isabelle] FMCAD 2025: Deadline Extension (1 message, latest: Apr 14 2025 at 11:03)
• [isabelle] New in the AFP: "First-Order Rewriting" and "P... (1 message, latest: Apr 13 2025 at 19:55)
• [isabelle] New in the AFP: Completeness of Decreasing Dia... (1 message, latest: Apr 13 2025 at 07:46)
• [isabelle] FM 2026: 1st Call for Papers (1 message, latest: Apr 10 2025 at 13:00)
• [isabelle] New in the AFP: Gyrovector Spaces (1 message, latest: Apr 09 2025 at 15:22)
• [isabelle] CICM 2025: 3rd Announcement and Call for Papers (1 message, latest: Apr 09 2025 at 06:38)
• [isabelle] FTfJP 2025 - Second Call for Papers (2 messages, latest: Apr 08 2025 at 18:11)
• [isabelle] UNIF 2025 2nd Call for Papers (1 message, latest: Apr 07 2025 at 18:13)
• [isabelle] Kleene Fixpoints (2 messages, latest: Apr 07 2025 at 06:22)
• [isabelle] superfluous assumption in Gcd_remove0_nat (2 messages, latest: Apr 05 2025 at 18:48)
• [isabelle] FSCD 2027: Call for Location (1 message, latest: Apr 03 2025 at 13:29)
• [isabelle] [PPDP 25] Second Call for Papers (1 message, latest: Apr 03 2025 at 11:19)
• [isabelle] New in the AFP: Morley's Theorem (1 message, latest: Apr 02 2025 at 00:28)
• [isabelle] Marktoberdorf Summer School 2025: call for par... (1 message, latest: Mar 31 2025 at 12:22)
• [isabelle] Professorhip in » Logic and Verification in Co... (1 message, latest: Mar 28 2025 at 12:14)
• [isabelle] Update of my gentle introduction (1 message, latest: Mar 27 2025 at 17:05)
• [isabelle] Call for papers: FCS @ CSF'25 (Extended deadli... (1 message, latest: Mar 26 2025 at 21:53)
• [isabelle] LSFA 2025 Second Call for Papers (1 message, latest: Mar 26 2025 at 21:53)
• [isabelle] LaTeX packages for greek and italicized letters (2 messages, latest: Mar 26 2025 at 21:13)
• [isabelle] Latex: Isabelle style packages not compatible ... (2 messages, latest: Mar 26 2025 at 10:29)
• [isabelle] Call for Participation: FORMALISE 2025 (2 messages, latest: Mar 25 2025 at 21:46)
• [isabelle] New in the AFP: Formal Proof of Dilworth's The... (1 message, latest: Mar 25 2025 at 13:17)
• [isabelle] 10 funded PhD positions in Automated Reasoning (1 message, latest: Mar 24 2025 at 12:32)
• [isabelle] Testing of verified software (2 messages, latest: Mar 24 2025 at 04:55)
• [isabelle] Impossible to insert the backslash character i... (2 messages, latest: Mar 23 2025 at 07:55)
• [isabelle] HCVS 2025 CfP: 12th Workshop on Horn Clauses f... (1 message, latest: Mar 21 2025 at 18:26)
• [isabelle] VSTTE 2025: First call for papers (1 message, latest: Mar 21 2025 at 18:26)
• [isabelle] Why Can't We Divide by Zero? (1 message, latest: Mar 21 2025 at 00:17)
• [isabelle] Strange behaviour with implicit coercions (2 messages, latest: Mar 20 2025 at 14:12)
• [isabelle] "Find facts" in Isabelle2025 (2 messages, latest: Mar 20 2025 at 11:09)
• [isabelle] [Hol-info] 2nd CfP - JELIA 2025 - 19th Europea... (1 message, latest: Mar 19 2025 at 10:49)
• [isabelle] ICE 2025: Second Call for Papers (1 message, latest: Mar 18 2025 at 20:15)
• [isabelle] ACL2-2025 Call for Participation (1 message, latest: Mar 18 2025 at 20:14)
• [isabelle] Midlands Graduate School 2025 final call -- re... (1 message, latest: Mar 18 2025 at 20:05)
• [isabelle] AFP 2025 (1 message, latest: Mar 17 2025 at 23:24)
• [isabelle] cl-isabelle-users Digest Thu, 13 Mar 2025 (1/1) (1 message, latest: Mar 17 2025 at 09:31)
• [isabelle] Announcing Isabelle2025 (1 message, latest: Mar 13 2025 at 16:28)
• [isabelle] Printing substitutions & Most General Unifier ... (2 messages, latest: Mar 13 2025 at 09:34)
• [isabelle] Call for papers: FCS @ CSF'25 (1 message, latest: Mar 12 2025 at 11:02)
• [isabelle] AITP 2025 - Call for Contributions (1 message, latest: Mar 12 2025 at 06:38)
• [isabelle] Call for Workshops, Conference on Intelligent ... (1 message, latest: Mar 11 2025 at 15:56)
• [isabelle] ITP 2025: Call for self-nomination of external... (1 message, latest: Mar 11 2025 at 13:54)
• [isabelle] IEEE SMC-IT/SCC 2025 CALL FOR SUBMISSIONS [UPDATE (1 message, latest: Mar 10 2025 at 17:40)
• [isabelle] Extracting current proof state via Isabelle/Scala (1 message, latest: Mar 10 2025 at 17:39)
• [isabelle] CFP: Collection on “Bridging Formal Verificati... (1 message, latest: Mar 08 2025 at 21:52)
• [isabelle] HOR 2025: Call for Papers (1 message, latest: Mar 08 2025 at 21:51)
• [isabelle] CfP RSSRail 2025, Int. Conf. on Reliability, S... (1 message, latest: Mar 08 2025 at 21:50)
• [isabelle] How to define parametric finite set of natural... (6 messages, latest: Mar 07 2025 at 01:08)
• [isabelle] FMCAD 2025 - 2nd Call for Papers (1 message, latest: Mar 06 2025 at 08:32)
• [isabelle] New in the AFP: Language Partitioning for Miss... (1 message, latest: Mar 04 2025 at 20:40)
• [isabelle] CALCO 2025: Deadline Extension (1 message, latest: Mar 04 2025 at 19:36)
• [isabelle] Isabelle2025-RC4: isabelle find_facts_server (1 message, latest: Mar 03 2025 at 18:47)
• [isabelle] Isabelle2025-RC4 available for serious applica... (1 message, latest: Mar 03 2025 at 18:26)
• [isabelle] EuroProofNet Symposium, 8-19 September 2025, 1... (1 message, latest: Mar 03 2025 at 16:07)
• [isabelle] ITP 2025: Second Call for Papers (1 message, latest: Mar 03 2025 at 12:38)
• [isabelle] a question about Build/export_theory.scala (4 messages, latest: Feb 27 2025 at 17:58)
• [isabelle] New in the AFP: Compactness Theorem for First-... (1 message, latest: Feb 27 2025 at 07:20)
• [isabelle] CALCO 2025: Final Call for Papers (1 message, latest: Feb 26 2025 at 13:30)
• [isabelle] MFPS 2025: Second Call for Papers (1 message, latest: Feb 26 2025 at 13:29)
• [isabelle] Postdoc position at LMU Munich (1 message, latest: Feb 25 2025 at 16:55)
• [isabelle] New AFP entry List_Power (1 message, latest: Feb 23 2025 at 00:55)
• [isabelle] New in the AFP: Quantum Fourier Transform (1 message, latest: Feb 21 2025 at 14:18)
• [isabelle] https://isabelle.in.tum.de/dist/library vs htt... (2 messages, latest: Feb 21 2025 at 10:40)
• [isabelle] Workshop on GenAI for Theorem Proving, Edinbur... (1 message, latest: Feb 21 2025 at 09:03)
• [isabelle] UNIF 2025 Call for Papers (1 message, latest: Feb 20 2025 at 21:13)
• [isabelle] Surprising `simp` behaviour for image-sets (8 messages, latest: Feb 20 2025 at 12:22)
• [isabelle] ICE 2025: First Call for Papers (1 message, latest: Feb 20 2025 at 11:46)
• [isabelle] Isabelle2025-RC2: Name-sensitivity of adhoc_ov... (3 messages, latest: Feb 20 2025 at 05:46)
• [isabelle] Isabelle2025-RC3 available for applications (1 message, latest: Feb 19 2025 at 15:01)
• [isabelle] Adhoc Overloading corrupted by unrelated defin... (3 messages, latest: Feb 19 2025 at 10:27)
• [isabelle] code_pred / inductive / lfp (6 messages, latest: Feb 18 2025 at 21:31)
• [isabelle] Isabelle2025-RC2 on windows (the extracting is... (2 messages, latest: Feb 18 2025 at 21:17)
• [isabelle] Printing of theorems in declare statement (3 messages, latest: Feb 18 2025 at 21:08)
• [isabelle] Registration now open -- Midlands Graduate Sch... (1 message, latest: Feb 18 2025 at 10:30)
• [isabelle] Isabelle2025-RC2 beanshell errors (10 messages, latest: Feb 17 2025 at 12:29)
• [isabelle] Unexpected warning about missing mapper function (2 messages, latest: Feb 17 2025 at 10:29)
• [isabelle] Followup: Unexpected warning about missing map... (2 messages, latest: Feb 17 2025 at 09:43)
• [isabelle] Isabelle2025-RC2 on windows: odd exceptions in... (2 messages, latest: Feb 16 2025 at 21:01)
• [isabelle] Isabelle2025-RC2 on windows (8 messages, latest: Feb 16 2025 at 18:59)
• [isabelle] Isabelle2025-RC2 UI possible error (3 messages, latest: Feb 15 2025 at 14:45)
• [isabelle] Second Announcement and CfP, Conference on Int... (1 message, latest: Feb 15 2025 at 13:53)
• [isabelle] CALL FOR IEEE SMC-IT/SCC 2025 SUBMISSIONS (1 message, latest: Feb 15 2025 at 11:52)
• [isabelle] Senior Lectureship and Lectureship in Cyber Se... (1 message, latest: Feb 15 2025 at 11:51)
• [isabelle] confusion with obtain (3 messages, latest: Feb 13 2025 at 10:55)
• [isabelle] Isabelle2025-RC2 VSCode sendback markup (1 message, latest: Feb 13 2025 at 08:59)
• [isabelle] Isabelle2025-RC2: PIDE completion mechanism (2 messages, latest: Feb 13 2025 at 00:30)
• [isabelle] FSCD 2025: Extended deadline (Abstract: Februa... (1 message, latest: Feb 12 2025 at 18:05)
• [isabelle] New in the AFP: A Proof of Hilbert Basis Theor... (1 message, latest: Feb 12 2025 at 08:34)
• [isabelle] Isabelle2025-RC1 hiding notation (3 messages, latest: Feb 11 2025 at 23:17)
• [isabelle] New in the AFP: Formalization of (Conflict-)Se... (1 message, latest: Feb 11 2025 at 12:22)
• [isabelle] JRE fatal error with Isabelle2025-RC1 (2 messages, latest: Feb 11 2025 at 11:34)
• [isabelle] Isabelle2025-RC1: Output dockable scroll position (2 messages, latest: Feb 10 2025 at 20:54)
• [isabelle] Isabelle2025-RC2 available for serious testing (1 message, latest: Feb 10 2025 at 12:44)
• [isabelle] Isabelle2025-RC1: issues with Command click th... (4 messages, latest: Feb 10 2025 at 01:50)
• [isabelle] Isabelle2025-RC1 Documentation Issues (4 messages, latest: Feb 08 2025 at 16:46)
• [isabelle] New in the AFP: Verification of the CVM algori... (1 message, latest: Feb 07 2025 at 16:55)
• [isabelle] 2025-RC1: Report of porting Isabelle-LLVM (2 messages, latest: Feb 07 2025 at 14:21)
• [isabelle] FSEN 2025 - Call for Participation (1 message, latest: Feb 07 2025 at 13:04)
• [isabelle] SPIN: Final Call for Papers (1 message, latest: Feb 07 2025 at 03:47)
• [isabelle] CALCO 2025: Second Call for Papers (1 message, latest: Feb 06 2025 at 15:41)
• [isabelle] Slow top-down contraction of abbreviations (3 messages, latest: Feb 06 2025 at 13:47)
• [isabelle] Issues with running Isabelle2024 (2 messages, latest: Feb 06 2025 at 11:27)
• [isabelle] PPDP 2025 Call for papers (1 message, latest: Feb 05 2025 at 11:14)
• [isabelle] PhD Position: Verification of Golang using Int... (1 message, latest: Feb 04 2025 at 11:08)
• [isabelle] 2025-RC1: issue with `inclduing` command (2 messages, latest: Feb 04 2025 at 10:15)
• [isabelle] Associate/Assistant professorship in Copenhage... (2 messages, latest: Feb 04 2025 at 09:19)
• [isabelle] beginner's syntax woes (5 messages, latest: Feb 03 2025 at 22:02)
• [isabelle] Isabelle2025-RC0: OpenJDK vs. RDP on Linux (2 messages, latest: Feb 03 2025 at 21:47)
• [isabelle] Isabelle2025-RC1 available for testing (1 message, latest: Feb 03 2025 at 19:22)
• [isabelle] Midlands Graduate School 2025 hosted by the Un... (1 message, latest: Feb 03 2025 at 14:36)
• [isabelle] How to parse theory files with Outer_Syntax.scala (5 messages, latest: Feb 03 2025 at 13:38)
• channel events (1 message, latest: Feb 03 2025 at 09:52)
• [isabelle] New in the AFP: Differential Privacy (using Qua... (1 message, latest: Feb 02 2025 at 21:26)
• [isabelle] cl-isabelle-users Digest Sun, 02 Feb 2025 (1/1) (1 message, latest: Feb 02 2025 at 05:44)
• [isabelle] New in the AFP: Transitive Union-Closed Families (1 message, latest: Feb 01 2025 at 13:29)
• [isabelle] Defining a model for a proof of independence o... (2 messages, latest: Feb 01 2025 at 09:16)
• [isabelle] How to generate / register a primitive recursi... (3 messages, latest: Feb 01 2025 at 08:25)
• [isabelle] Using Isabelle to show which assumptions are n... (11 messages, latest: Jan 30 2025 at 00:10)
• [isabelle] Notation for "concat(replicate n xs)" (12 messages, latest: Jan 29 2025 at 14:03)
• [isabelle] New in the AFP x 2 (1 message, latest: Jan 28 2025 at 18:47)
• [isabelle] LSFA 2025 Call for Papers (1 message, latest: Jan 27 2025 at 21:37)
• [isabelle] ITP 2025: First Call for Papers (1 message, latest: Jan 25 2025 at 15:36)
• [isabelle] New in the AFP: The Rogers–Ramanujan Identitie... (1 message, latest: Jan 24 2025 at 13:55)
• [isabelle] New in the AFP: Negatively Associated Random V... (1 message, latest: Jan 20 2025 at 09:21)
• [isabelle] FMCAD 2025 - Call for Papers (1 message, latest: Jan 19 2025 at 16:37)
• [isabelle] First CfP - JELIA 2025 - 19th European Confere... (1 message, latest: Jan 18 2025 at 13:04)
• [isabelle] New in the AFP: Burrows–Wheeler Transform (1 message, latest: Jan 17 2025 at 12:16)
• [isabelle] FMBC25 - Second Call for Papers (1 message, latest: Jan 17 2025 at 10:03)
• [isabelle] Workshop on Theorem Proving and Machine Learni... (2 messages, latest: Jan 15 2025 at 20:39)
• [isabelle] Job Ad: Proof Engineer at Cryspen (1 message, latest: Jan 15 2025 at 17:00)
• [isabelle] Dahl-Nygaard junior and senior prizes 2025 - d... (1 message, latest: Jan 15 2025 at 17:00)
• [isabelle] Postdoctoral Research Fellow (1 message, latest: Jan 13 2025 at 11:38)
• [isabelle] OPLSS 2025 (1 message, latest: Jan 12 2025 at 14:34)
• [isabelle] Isabelle Package Manager Survey (5 messages, latest: Jan 11 2025 at 12:07)
• [isabelle] mispaced "and" in Product_Type.thy (2 messages, latest: Jan 10 2025 at 15:39)
• [isabelle] Divides / Euclidean_Rings (1 message, latest: Jan 09 2025 at 09:16)
• [isabelle] Isabelle2025-RC0 available for early experimen... (11 messages, latest: Jan 09 2025 at 09:12)
• [isabelle] Final call for participation: LMS/BCS-FACS Onl... (1 message, latest: Jan 09 2025 at 01:21)
• [isabelle] Code check failed for Haskell: (7 messages, latest: Jan 07 2025 at 19:37)
• [isabelle] invoking sledgehammer via command line (1 message, latest: Jan 07 2025 at 15:03)
• [isabelle] New in the AFP: the existence of God (again) (1 message, latest: Jan 07 2025 at 13:11)
• [isabelle] invoking sledgehammer via command line (1 message, latest: Jan 07 2025 at 13:03)
• [isabelle] subgroup generates itself (1 message, latest: Jan 06 2025 at 15:27)
• [isabelle] VSS 2025: Call for Papers (1 message, latest: Jan 05 2025 at 14:46)
• [isabelle] Incomplete abbreviation folding in stacked abb... (1 message, latest: Dec 29 2024 at 16:36)
• [isabelle] ECOOP 2025: Call for Papers (1 message, latest: Dec 27 2024 at 19:17)
• [isabelle] New in the AFP: A Generalization of the Cauchy... (1 message, latest: Dec 27 2024 at 12:31)
• [isabelle] MFPS 2025: Call for Papers (1 message, latest: Dec 20 2024 at 14:03)
• [isabelle] CALCO 2025: Call for Papers (1 message, latest: Dec 20 2024 at 13:50)
• [isabelle] PhD position on model checking of functional p... (1 message, latest: Dec 18 2024 at 13:12)
• [isabelle] Postdoc position in formal methods for securit... (1 message, latest: Dec 18 2024 at 13:12)
• [isabelle] [TFP (and TFPiE) 2025] Call For Participation ... (1 message, latest: Dec 18 2024 at 08:12)
• [isabelle] LMS/BCS-FACS Online Seminar, Annabelle McIver,... (1 message, latest: Dec 16 2024 at 21:45)
• [isabelle] [CPP'25] Call for Participation: Certified Pro... (1 message, latest: Dec 12 2024 at 19:38)
• [isabelle] System stuck after try0 calls in separate thread (5 messages, latest: Dec 11 2024 at 15:17)
• [isabelle] Renaming of bound variables with structural lo... (4 messages, latest: Dec 11 2024 at 10:54)
• [isabelle] FSCD 2025: Second Call for Papers (1 message, latest: Dec 10 2024 at 14:13)
• [isabelle] Announcement and CfP, Conference on Intelligen... (1 message, latest: Dec 09 2024 at 09:05)
• [isabelle] FMBC - First Call for Papers (1 message, latest: Dec 06 2024 at 15:18)
• [isabelle] AI for Math Fund announcement (1 message, latest: Dec 05 2024 at 20:09)
• [isabelle] New in the AFP: The Tensor Product on Hilbert ... (1 message, latest: Dec 04 2024 at 17:57)
• [isabelle] Running some ml code without storing the bindings (2 messages, latest: Dec 03 2024 at 06:05)
• [isabelle] New in the AFP: The Sum-of-Squares Function an... (1 message, latest: Nov 30 2024 at 11:23)
• [isabelle] a little typo in a tutorial (2 messages, latest: Nov 29 2024 at 09:47)
• [isabelle] New in the AFP: ILL and Linear Resources and P... (1 message, latest: Nov 28 2024 at 15:55)
• [isabelle] New in the AFP: Dissection of a Cube (1 message, latest: Nov 25 2024 at 16:34)
• [isabelle] New in the AFP: Two Theorems on Hermitian Matr... (1 message, latest: Nov 25 2024 at 16:08)
• [isabelle] A problem with the "tactic" method (2 messages, latest: Nov 23 2024 at 12:13)
• [isabelle] auto raising Interrupt_Breakdown (1 message, latest: Nov 22 2024 at 18:45)
• [isabelle] HOL-Analysis bug reminder (10 messages, latest: Nov 22 2024 at 14:57)
• [isabelle] Interrupt_Breakdown exception for function (do... (5 messages, latest: Nov 21 2024 at 14:52)
• [isabelle] Duplicate theory name Discrete (21 messages, latest: Nov 19 2024 at 13:17)
• [isabelle] Calculation of Lebesgue-Stieltjes Integral (2 messages, latest: Nov 19 2024 at 12:56)
• [isabelle] SPIN 2025: Call for Papers (1 message, latest: Nov 18 2024 at 05:02)
• [isabelle] [TFP 2025 3rd Call for Papers] 25th Internatio... (1 message, latest: Nov 15 2024 at 14:13)
• [isabelle] tag invisible and qed (1 message, latest: Nov 14 2024 at 10:46)
• [isabelle] Final Call for Papers: FORMALISE 2025 - EXTEND... (1 message, latest: Nov 12 2024 at 19:14)
• [isabelle] [Announcement] An unofficial REPL server for I... (1 message, latest: Nov 12 2024 at 14:42)
• [isabelle] Printing constants (6 messages, latest: Nov 08 2024 at 12:22)
• [isabelle] Type of constant map (1 message, latest: Nov 08 2024 at 12:18)
• [isabelle] Support for forget structure in user defined M... (1 message, latest: Nov 07 2024 at 16:11)
• [isabelle] PriSC @ POPL'25: Extended deadline (1 message, latest: Nov 05 2024 at 17:16)
• [isabelle] New in the AFP: SCL Simulates Nonredundant Gro... (1 message, latest: Nov 04 2024 at 15:11)
• [isabelle] New in the AFP: The Boustrophedon Transform (1 message, latest: Nov 01 2024 at 15:20)
• [isabelle] New in the AFP: Babai's Nearest Plane Algorithm (1 message, latest: Oct 31 2024 at 10:39)
• [isabelle] New in the AFP: A Modular Formalization of Sup... (1 message, latest: Oct 30 2024 at 12:19)
• [isabelle] New in the AFP: Minimal, Maximal, Least, and G... (1 message, latest: Oct 30 2024 at 06:58)
• [isabelle] Isabelle Projects page (2 messages, latest: Oct 29 2024 at 11:37)
• [isabelle] isabelle vscode broken on windows - path issue (1 message, latest: Oct 29 2024 at 10:04)
• [isabelle] Call for Papers - Special Issue of JLAMP on Re... (1 message, latest: Oct 28 2024 at 16:24)
• [isabelle] typedecl with class (1 message, latest: Oct 27 2024 at 18:57)
• [isabelle] space for \<^latex> notation (3 messages, latest: Oct 26 2024 at 12:22)
• [isabelle] Unexpected behavior when recursively importing... (4 messages, latest: Oct 24 2024 at 15:34)
• [isabelle] FSCD 2025: Call for Workshop Proposals (1 message, latest: Oct 21 2024 at 18:17)
• [isabelle] PriSC @ POPL'25: 2nd Call for Paper (1 message, latest: Oct 21 2024 at 10:33)
• [isabelle] Isabelle/ML - Theorem and Local Theories (7 messages, latest: Oct 18 2024 at 21:59)
• [isabelle] FSCD 2025: First Call for Papers (1 message, latest: Oct 18 2024 at 11:25)
• [isabelle] POPL 2025 Call for Tutorials (deadline extende... (1 message, latest: Oct 17 2024 at 21:35)
• [isabelle] New in the AFP: Wooley's Discrete Inequality (1 message, latest: Oct 17 2024 at 13:20)
• [isabelle] CiE 2025, 14-18 July 2025, Lisbon (Portugal) -... (1 message, latest: Oct 17 2024 at 07:46)
• [isabelle] New in the AFP: the category of sets (1 message, latest: Oct 11 2024 at 14:54)
• [isabelle] [TFP 2025 2nd Call for Papers] 25th Internatio... (1 message, latest: Oct 11 2024 at 13:40)
• [isabelle] New in the AFP: The Karatsuba Square Root Algo... (1 message, latest: Oct 09 2024 at 13:33)
• [isabelle] Assistant Professor (Tenure Track) position at... (1 message, latest: Oct 09 2024 at 12:42)
• [isabelle] PhD and postdoc position at the University of ... (1 message, latest: Oct 09 2024 at 08:30)
• [isabelle] Dafny Workshop at POPL 2025 (deadline extension) (1 message, latest: Oct 08 2024 at 22:08)
• [isabelle] Formalisation of mathematics with interactive ... (1 message, latest: Oct 08 2024 at 17:20)
• [isabelle] FSEN 2025 - Final Call for Papers (Deadline ex... (1 message, latest: Oct 07 2024 at 08:29)
• [isabelle] Looking for Transfer Package Introduction in I... (3 messages, latest: Oct 04 2024 at 09:28)
• [isabelle] New in the AFP: Abstract Substitution (1 message, latest: Oct 04 2024 at 08:40)
• [isabelle] Logic Summer School at Australian National Uni... (1 message, latest: Oct 04 2024 at 02:29)
• [isabelle] Running Isabelle on Linux with musl libc (4 messages, latest: Oct 03 2024 at 21:04)
• [isabelle] base session in ROOT file for AFP submission (2 messages, latest: Oct 03 2024 at 13:22)
• [isabelle] Call for Papers: FORMALISE 2025 (1 message, latest: Oct 03 2024 at 12:44)
• [isabelle] New in the AFP: Formally Verified Suffix Array... (1 message, latest: Oct 03 2024 at 00:25)
• [isabelle] New in the AFP: Parallel Shear Sort (1 message, latest: Sep 30 2024 at 14:29)
• [isabelle] Size-Function for datatypes (2 messages, latest: Sep 26 2024 at 16:14)
• [isabelle] New in the AFP: Rabin's Closest Pair of Points... (1 message, latest: Sep 23 2024 at 10:13)
• [isabelle] Workshop on "Big Specification: Specification,... (1 message, latest: Sep 22 2024 at 08:44)
• [isabelle] New in the AFP: NREST: Nondeterministc RESsult... (1 message, latest: Sep 18 2024 at 09:46)
• [isabelle] left vector multiplication not associative (a ... (1 message, latest: Sep 17 2024 at 07:22)
• [isabelle] New in the AFP: Concrete bounds for Chebyshev’... (1 message, latest: Sep 16 2024 at 15:44)
• [isabelle] New in the AFP: Verifying a Decision Procedure... (1 message, latest: Jun 03 2024 at 16:26)
• [isabelle] deadline extended: LSFA 2024 (1 message, latest: Jun 03 2024 at 10:22)
• [isabelle] Postdoctoral Research Fellow at the University... (1 message, latest: Jun 03 2024 at 08:38)
• [isabelle] Example Projects manipulating Isabelle/Scala, ... (4 messages, latest: Jun 02 2024 at 09:51)
• Your bouncing address in list cl-isabelle-users (2 messages, latest: Jun 01 2024 at 18:08)
• [isabelle] PhD Positions Available at the University of L... (1 message, latest: May 31 2024 at 16:40)
• [isabelle] Special syntax for a binder (4 messages, latest: May 31 2024 at 10:02)
• [isabelle] Record package and user qualifier support (2 messages, latest: May 31 2024 at 09:12)
• [isabelle] International Conference on Artificial Intelli... (3 messages, latest: May 28 2024 at 20:52)
• [isabelle] Isabelle Workshop 2024: date change (1 message, latest: May 28 2024 at 19:31)
• [isabelle] New in the AFP: AutoCorres2 (8 messages, latest: May 27 2024 at 18:11)
• [isabelle] AFP 2024 (1 message, latest: May 26 2024 at 09:58)
• [isabelle] Sluggish Isabelle/jEdit experience with extern... (6 messages, latest: May 26 2024 at 09:26)
• [isabelle] PLMW@ICFP'24: Call for Participation (travel f... (1 message, latest: May 24 2024 at 19:52)
• [isabelle] Announcing Isabelle2024 (2 messages, latest: May 24 2024 at 09:18)
• [isabelle] How to obtain LaTeX source from failed documen... (4 messages, latest: May 23 2024 at 20:38)
• [isabelle] StackOverflowError when traversing PIDE markup (2 messages, latest: May 23 2024 at 15:26)
• [isabelle] Call for Submissions to the Doctoral Program -... (1 message, latest: May 23 2024 at 06:45)
• [isabelle] FACS 2024 - Third Call for Papers (1 message, latest: May 07 2024 at 09:38)
• [isabelle] Call for Papers: the 5th International Worksho... (1 message, latest: May 06 2024 at 11:37)
• [isabelle] SAT/SMT/AR Summer School 2024: June 26-29 (1 message, latest: May 06 2024 at 11:07)
• [isabelle] Folding pretty-printed output by default (1 message, latest: May 06 2024 at 05:35)
• [isabelle] WAIT2024 Call for Abstracts: Fifth Internation... (1 message, latest: May 05 2024 at 22:06)
• [isabelle] How to debug the auto method? (3 messages, latest: May 05 2024 at 11:53)
• [isabelle] Strange errors by coinductive command with boo... (1 message, latest: May 05 2024 at 09:03)
• [isabelle] Coinductive (beginners?) question (5 messages, latest: May 05 2024 at 06:55)
• [isabelle] Meta-implication in a premise (14 messages, latest: May 04 2024 at 17:20)
• [isabelle] New in the AFP: Substitutions for Lambda-Free ... (1 message, latest: May 03 2024 at 17:38)
• [isabelle] Position: Full Professor in Programming Langua... (1 message, latest: May 03 2024 at 11:08)
• [isabelle] New in the AFP: Undecidability Results on Orie... (1 message, latest: May 03 2024 at 09:32)
• [isabelle] [Isabelle2024-RC3] Open reports regarding code... (2 messages, latest: May 03 2024 at 09:19)
• [isabelle] AITP 2024 FINAL CALL FOR CONTRIBUTIONS - EXTEN... (1 message, latest: May 03 2024 at 08:16)
• [isabelle] Isabelle2024-RC3 available for testing and app... (1 message, latest: May 02 2024 at 18:45)
• [isabelle] New in the AFP: Derandomization with Condition... (1 message, latest: May 02 2024 at 15:19)
• [isabelle] New in the AFP: Pick's Theorem (1 message, latest: May 01 2024 at 13:43)
• [isabelle] International Intelligence, Sustainability, an... (1 message, latest: Apr 30 2024 at 15:06)
• [isabelle] 2024 Formal Methods in Computer-Aided Design (... (2 messages, latest: Apr 30 2024 at 05:09)
• [isabelle] PPDP 2024 - Final CFP (1 message, latest: Apr 29 2024 at 20:08)
• [isabelle] ConcurrentModificationException in UI Code [wa... (3 messages, latest: Apr 26 2024 at 14:59)
• [isabelle] Extremely slow HOL heap builds with Isabelle20... (3 messages, latest: Apr 25 2024 at 20:52)
• [isabelle] Future theorem equality: bad prop for alpha-et... (5 messages, latest: Apr 24 2024 at 15:29)
• [isabelle] Meta-implication as part of a goal (3 messages, latest: Apr 23 2024 at 21:27)
• [isabelle] ICTAC 2024 - Second Call for Papers (1 message, latest: Apr 23 2024 at 11:36)
• [isabelle] Spurious performance loss in Isabelle2023 (4 messages, latest: Apr 23 2024 at 03:38)
• [isabelle] Malformed theory files in Isabelle/src (4 messages, latest: Apr 22 2024 at 12:23)
• [isabelle] Submitting my proof to AFP (4 messages, latest: Apr 22 2024 at 08:28)
• [isabelle] afp 2024 fork approaching (2 messages, latest: Apr 22 2024 at 03:35)
• [isabelle] Isabelle AFP submission says "Invalid Request" (1 message, latest: Apr 20 2024 at 04:32)
• [isabelle] New in the AFP: A Verified Proof Checker for M... (1 message, latest: Apr 19 2024 at 11:34)
• [isabelle] Isabelle2024-RC2 available for testing (and ea... (1 message, latest: Apr 18 2024 at 14:10)
• [isabelle] IJCAR 2024: Call for Participation (1 message, latest: Apr 18 2024 at 13:06)
• [isabelle] 31st Static Analysis Symposium (SAS 2024) : Ca... (1 message, latest: Apr 18 2024 at 12:07)
• [isabelle] ARQNL 2024 - Final Call for Papers (1 message, latest: Apr 17 2024 at 14:08)
• [isabelle] New in the AFP: ConcurrentHOL (1 message, latest: Apr 17 2024 at 08:04)
• [isabelle] Odd exception in function package (2 messages, latest: Apr 15 2024 at 12:42)
• [isabelle] hide_facts in Group.thy (6 messages, latest: Apr 15 2024 at 06:53)
• [isabelle] HOL-Analysis: definition of "C1_differentiable... (4 messages, latest: Apr 14 2024 at 23:40)
• [isabelle] How to resolve the FUNCTION_BODY_NOT_IN_INPUT_... (1 message, latest: Apr 12 2024 at 15:57)
• [isabelle] FACS 24 - Second Call for Papers (1 message, latest: Apr 11 2024 at 07:48)
• [isabelle] formal Mechanics (3 messages, latest: Apr 10 2024 at 11:23)
• [isabelle] Multiple PhD and postdoc positions in PL/FM at... (1 message, latest: Apr 10 2024 at 05:47)
• [isabelle] UNIF 2024 - 2nd Call for Papers (Extended Dead... (1 message, latest: Apr 09 2024 at 15:06)
• [isabelle] ICFP Programming Contest 2024 (1 message, latest: Apr 08 2024 at 10:37)
• [isabelle] New in the AFP: Uncertainty Principle (1 message, latest: Apr 08 2024 at 10:34)
• [isabelle] IJCAR: Woody Bledsoe Award: Call for Nominations (1 message, latest: Apr 08 2024 at 09:08)
• [isabelle] Isabelle2024-RC1: Compiling generated Scala co... (4 messages, latest: Apr 05 2024 at 15:58)
• [isabelle] MARKTOBERDORF SUMMER SCHOOL 2024: CALL FOR PAR... (1 message, latest: Apr 05 2024 at 15:06)
• [isabelle] 回复： Why is the subgoal still unable to be veri... (2 messages, latest: Apr 04 2024 at 15:40)
• [isabelle] Isabelle2024-RC1 available for testing (1 message, latest: Apr 03 2024 at 13:24)
• [isabelle] 5th International Workshop on Formal Methods f... (1 message, latest: Apr 03 2024 at 08:41)
• [isabelle] New in the AFP: Broadcast Psi-calculi (2 messages, latest: Apr 02 2024 at 15:43)
• [isabelle] SAT/SMT/AR Summer School 2024 - Call for Appli... (1 message, latest: Apr 02 2024 at 07:06)
• [isabelle] Why is the subgoal still unable to be verified... (3 messages, latest: Apr 01 2024 at 10:17)
• [isabelle] ARQNL 2024 - Call for Papers (1 message, latest: Mar 31 2024 at 09:31)
• [isabelle] FM 2024: Call for Papers (2 messages, latest: Mar 30 2024 at 21:31)
• [isabelle] PostDoc in using Formal Methods for finding se... (1 message, latest: Mar 30 2024 at 11:12)
• [isabelle] New in the AFP: Doob's Upcrossing Inequality a... (1 message, latest: Mar 29 2024 at 22:02)
• [isabelle] New in the AFP: Kummer's congruence (1 message, latest: Mar 29 2024 at 12:48)
• [isabelle] New in the AFP: Conditional normative reasoning (1 message, latest: Mar 29 2024 at 12:30)
• [isabelle] case_names for induction rule (3 messages, latest: Mar 28 2024 at 09:27)
• [isabelle] LSFA 2024: CALL FOR PAPERS (1 message, latest: Mar 27 2024 at 22:50)
• [isabelle] ICE 2024: Third Call for Papers (abstract dead... (1 message, latest: Mar 26 2024 at 16:52)
• [isabelle] TyDe 2024: First call for papers and extended ... (1 message, latest: Mar 26 2024 at 16:51)
• [isabelle] ISR 2024: Call for Participation (1 message, latest: Mar 26 2024 at 08:56)
• [isabelle] Extended Deadline April 8, 2024 (abstracts Apr... (1 message, latest: Mar 26 2024 at 08:23)
• [isabelle] Contribution proposal to Isabelle documentation (2 messages, latest: Mar 25 2024 at 15:50)
• [isabelle] ThEdu'24 - 2nd Call for Extended Abstracts (1 message, latest: Mar 25 2024 at 15:44)
• [isabelle] New in the AFP: Continued Fractions (1 message, latest: Mar 25 2024 at 15:42)
• [isabelle] New in the AFP: Approximate Model Counting (1 message, latest: Mar 25 2024 at 15:42)
• [isabelle] New Journal: Annals of Formalized Mathematics (1 message, latest: Mar 23 2024 at 04:19)
• [isabelle] 20 Years of the AFP (1 message, latest: Mar 22 2024 at 21:33)
• [isabelle] Annals of Formalized Mathematics (1 message, latest: Mar 22 2024 at 14:39)
• [isabelle] [PPDP'2024 CfP] The 26th International Symposi... (1 message, latest: Mar 21 2024 at 14:35)
• [isabelle] Funded PhD Position in Formalizing/Verificatio... (1 message, latest: Mar 20 2024 at 16:46)
• [isabelle] PhD / Postdoc positions related to quantum ver... (1 message, latest: Mar 19 2024 at 16:18)
• [isabelle] Postdoc/Research associate position in modal t... (1 message, latest: Mar 15 2024 at 17:42)
• [isabelle] Final Call for Papers: 17th Conference on Inte... (1 message, latest: Mar 15 2024 at 07:41)
• [isabelle] Fact names used by sledgehammer proof reconstr... (10 messages, latest: Mar 14 2024 at 14:47)
• [isabelle] AITP 2024 - Call for Contributions (1 message, latest: Mar 12 2024 at 02:59)
• [isabelle] New in the AFP: Go Code Generation for Isabelle (1 message, latest: Mar 11 2024 at 11:00)
• [isabelle] Fields of a record (3 messages, latest: Mar 11 2024 at 09:19)
• [isabelle] Installing Linter (5 messages, latest: Mar 11 2024 at 08:28)
• [isabelle] New in the AFP: Operational Semantics formally... (1 message, latest: Mar 08 2024 at 11:08)
• [isabelle] New in the AFP: The Wieferich–Kempner Theorem ... (1 message, latest: Mar 08 2024 at 09:06)
• [isabelle] New in the AFP: Verified QBF Solving (1 message, latest: Mar 08 2024 at 09:01)
• [isabelle] RC3: F# not mentioned in Isabelle overview (5 messages, latest: Mar 07 2024 at 17:14)
• [isabelle] Isabelle2024-RC0: official support for arm64-l... (2 messages, latest: Mar 06 2024 at 20:58)
• [isabelle] Release Candidates for Isabelle2024 (1 message, latest: Mar 06 2024 at 10:40)
• [isabelle] ITP 2024, Interactive Theorem Proving: Last Ca... (1 message, latest: Mar 05 2024 at 13:40)
• [isabelle] New in the AFP: Cubical Categories (1 message, latest: Mar 04 2024 at 15:13)
• [isabelle] Symbolic Computation in Software Science (SCSS... (1 message, latest: Mar 04 2024 at 06:56)
• [isabelle] Dov Gabbay Prize 2024: Call for Nominations (1 message, latest: Mar 02 2024 at 19:25)
• [isabelle] Unexpected(?) behaviour of polymorphic constants (3 messages, latest: Mar 02 2024 at 13:37)
• [isabelle] HOL-Library.Array_Braun declares Let_def as si... (9 messages, latest: Mar 01 2024 at 14:20)
• [isabelle] Isabelle nondetermistically reports error at e... (5 messages, latest: Feb 28 2024 at 19:58)
• [isabelle] ICE 2024: Second Call for Papers (1 message, latest: Feb 28 2024 at 18:19)
• [isabelle] Interactive theorem proving internship at AWS ... (1 message, latest: Feb 28 2024 at 15:25)
• [isabelle] Job offer / Researcher-Engineer / Inria & LMF,... (1 message, latest: Feb 26 2024 at 10:38)
• [isabelle] Issues with Formal Verification of C Programs ... (1 message, latest: Feb 24 2024 at 10:07)
• [isabelle] ITP 2024: Call for Workshop and Tutorial Propo... (2 messages, latest: Feb 24 2024 at 04:16)
• [isabelle] CfP: SCSS 2024 (1 message, latest: Feb 23 2024 at 21:51)
• [isabelle] PhD position at the University of Copenhagen (2 messages, latest: Feb 22 2024 at 12:00)
• [isabelle] New in the AFP: Karatsuba Multiplication on In... (1 message, latest: Feb 20 2024 at 15:07)
• [isabelle] `lift_definition (code_dt)` with type classes (1 message, latest: Feb 18 2024 at 05:13)
• [isabelle] Constant folding during code generation from l... (6 messages, latest: Feb 18 2024 at 05:02)
• [isabelle] Erratum: Post-doctoral position in mechanized ... (1 message, latest: Feb 16 2024 at 21:30)
• [isabelle] Call for Bids to Host FroCoS-ITP-TABLEAUX 2025 (1 message, latest: Feb 16 2024 at 13:44)
• [isabelle] Post-doctoral position in mechanized theorem p... (2 messages, latest: Feb 16 2024 at 11:21)
• [isabelle] ITP 2024 : Second call for papers (1 message, latest: Feb 16 2024 at 07:46)
• [isabelle] VerifyThis 2024 : Call for Participation (1 message, latest: Feb 15 2024 at 15:57)
• [isabelle] 2024 Summer School on Formal Techniques, Ather... (1 message, latest: Feb 14 2024 at 13:04)
• [isabelle] Call for Papers: Mathematics in Artificial Int... (1 message, latest: Feb 14 2024 at 13:03)
• [isabelle] Formal verification for organic synthesis? (5 messages, latest: Feb 14 2024 at 11:10)
• [isabelle] New in the AFP: Information Flow Control via S... (1 message, latest: Feb 13 2024 at 11:55)
• [isabelle] CFP PPDP 2024 - The 26th International Symposi... (1 message, latest: Feb 12 2024 at 11:56)
• [isabelle] The set difference operator symbol (8 messages, latest: Feb 12 2024 at 10:23)
• [isabelle] Code generation for compound types with invariant (7 messages, latest: Feb 10 2024 at 08:03)
• [isabelle] Isabelle/HOL at AWS (3 messages, latest: Feb 10 2024 at 00:37)
• [isabelle] CfP: Logica Frameworks and Meta Languages: The... (1 message, latest: Feb 08 2024 at 22:32)
• [isabelle] ICTAC 2024: First call for papers (1 message, latest: Feb 07 2024 at 11:15)
• [isabelle] New in the AFP: The Sumcheck Protocol (1 message, latest: Feb 07 2024 at 08:12)
• [isabelle] FSCD 2024: Extended deadline (Abstract: Februa... (1 message, latest: Feb 06 2024 at 18:30)
• [isabelle] how to run exercises on Windows (6 messages, latest: Feb 05 2024 at 07:46)
• [isabelle] Declaring a type of polymorphic fixed-length l... (6 messages, latest: Feb 02 2024 at 06:13)
• [isabelle] First Call for Papers - 20th International Con... (1 message, latest: Feb 01 2024 at 14:58)
• [isabelle] Strictness of adhoc_overloading in locale hier... (2 messages, latest: Feb 01 2024 at 12:53)
• [isabelle] [CFP] HCVS24 - Deadline extension 18/02/2024 (1 message, latest: Feb 01 2024 at 11:18)
• [isabelle] New in the AFP: Higher Globular Catoids and Qu... (1 message, latest: Feb 01 2024 at 07:30)
• [isabelle] Last Call (deadline Jan 31): School of Formali... (2 messages, latest: Jan 31 2024 at 15:05)
• [isabelle] New in the AFP: Region Quadtrees (1 message, latest: Jan 31 2024 at 13:49)
• [isabelle] exception TYPE when instantiating type variabl... (3 messages, latest: Jan 29 2024 at 11:34)
• [isabelle] Relaxing type class constraints on interval mu... (2 messages, latest: Jan 25 2024 at 21:09)
• [isabelle] ThEdu'24 - Open Call for Extended Abstracts (1 message, latest: Jan 25 2024 at 19:16)
• [isabelle] FMBC 2024 – Fourth Call for Papers (deadline e... (1 message, latest: Jan 25 2024 at 11:00)
• [isabelle] PAAR 2024, Call for Papers: 9th Workshop on Pr... (1 message, latest: Jan 25 2024 at 07:50)
• [isabelle] 2nd Call for Papers: 17th Conference on Intell... (1 message, latest: Jan 24 2024 at 16:18)
• [isabelle] Screenshot from 2024-01-23 23-41-07 (3 messages, latest: Jan 24 2024 at 15:12)
• [isabelle] Isabelle not work with vscode (2 messages, latest: Jan 24 2024 at 11:16)
• [isabelle] New in the AFP: Decomposition of totally order... (1 message, latest: Jan 23 2024 at 12:01)
• [isabelle] Bad theory import (3 messages, latest: Jan 22 2024 at 21:48)
• [isabelle] New in the AFP: Extended Interval Analysis (1 message, latest: Jan 22 2024 at 16:07)
• [isabelle] Postdoctoral position on Program Semantics and... (2 messages, latest: Jan 22 2024 at 13:37)
• [isabelle] reviewing Isabelle proofs in industry (1 message, latest: Jan 19 2024 at 14:06)
• [isabelle] UNIF 2024 Call for Papers (1 message, latest: Jan 18 2024 at 15:37)
• [isabelle] PhD position in Formal Methods at the Univers... (1 message, latest: Jan 18 2024 at 14:50)
• [isabelle] CICM 2024, Call for Workshop and Tutorial Prop... (1 message, latest: Jan 16 2024 at 16:29)
• [isabelle] New in teh AFP: CRYSTALS-Kyber_Security (1 message, latest: Jan 16 2024 at 14:41)
• [isabelle] [EXT] consumes and cases (1 message, latest: Jan 16 2024 at 13:50)
• [isabelle] Segmentation fault in verit invoked by try (3 messages, latest: Jan 16 2024 at 08:37)
• [isabelle] FMBC 2024 - Third Call for Papers (1 message, latest: Jan 15 2024 at 13:45)
• [isabelle] ICE 2024: First Call for Papers (1 message, latest: Jan 14 2024 at 11:41)
• [isabelle] consumes and cases (3 messages, latest: Jan 12 2024 at 17:39)
• [isabelle] Minor Error in Isabelle Referece Manual (2 messages, latest: Jan 12 2024 at 16:17)
• [isabelle] Job ad: Lecturer in Computer Science, Royal Ho... (1 message, latest: Jan 12 2024 at 14:29)
• [isabelle] Cambridge seminar series "Formalisation of ma... (1 message, latest: Jan 12 2024 at 13:29)
• [isabelle] Isabelle/ML: plain string representation for a... (8 messages, latest: Jan 12 2024 at 13:28)
• [isabelle] Trouble understanding Nitpick result (3 messages, latest: Jan 12 2024 at 08:33)
• [isabelle] IJCAR 2024: Final Call for Papers (1 message, latest: Jan 11 2024 at 23:33)
• [isabelle] FSCD 2024: Second Call for Papers (1 message, latest: Jan 11 2024 at 18:01)
• [isabelle] Missing list lemma (6 messages, latest: Jan 11 2024 at 10:26)
• [isabelle] Simple small example -- running into problems (8 messages, latest: Jan 10 2024 at 11:24)
• [isabelle] Assistant/Associate/Full professorship in Cope... (1 message, latest: Jan 08 2024 at 16:19)
• [isabelle] LMS/BCS-FACS online talk by Lawrence Paulson, ... (2 messages, latest: Jan 08 2024 at 12:47)
• [isabelle] Unexpected Behavior with Isabelle Server 2023 (1 message, latest: Jan 08 2024 at 09:44)
• [isabelle] Several remarks on CZH (AFP) (1 message, latest: Jan 01 2024 at 23:54)
• [isabelle] How to verify a C program with Isabelle (9 messages, latest: Dec 26 2023 at 20:51)
• [isabelle] [TFP (and TFPiE) 2024] Call For Participation ... (1 message, latest: Dec 22 2023 at 13:23)
• [isabelle] Interactions Between Proof Assistants and Math... (2 messages, latest: Dec 19 2023 at 11:24)
• [isabelle] Lean Together 2024 (1 message, latest: Dec 17 2023 at 22:56)
• [isabelle] FMBC 2024 - Second Call for Papers (1 message, latest: Dec 15 2023 at 15:25)
• [isabelle] New in the AFP: Knuth–Morris–Pratt String Search (1 message, latest: Dec 12 2023 at 14:03)
• [isabelle] ITP 2024: First Call for Papers (1 message, latest: Dec 12 2023 at 10:26)
• [isabelle] Full Professorship in Formal Methods at the Jo... (1 message, latest: Dec 11 2023 at 17:19)
• [isabelle] Certified Programs and Proofs (CPP'24) - Call ... (1 message, latest: Dec 11 2023 at 10:50)
• [isabelle] How to pretty-print definitions? type-synonyms? (1 message, latest: Dec 09 2023 at 20:55)
• [isabelle] New in the AFP: HOL-CSPM by Ballenghien, Taha ... (1 message, latest: Dec 09 2023 at 18:55)
• [isabelle] _update_name - where is it defined/documented (5 messages, latest: Dec 08 2023 at 10:37)
• [isabelle] Strange failure of datatype definition (5 messages, latest: Dec 07 2023 at 07:05)
• [isabelle] Referencing chained facts after "unfolding" (1 message, latest: Dec 06 2023 at 11:47)
• [isabelle] New in the AFP: Martingales (1 message, latest: Dec 06 2023 at 00:32)
• [isabelle] New in the AFP: Concentration Inequalities (1 message, latest: Dec 05 2023 at 23:46)
• [isabelle] New in the AFP: Lambert Series (1 message, latest: Nov 28 2023 at 18:11)
• [isabelle] IJCAR 2024: 2nd Call for Papers (1 message, latest: Nov 27 2023 at 19:20)
• [isabelle] IJCAR 2024: 2nd call for co-located events (1 message, latest: Nov 27 2023 at 14:27)
• [isabelle] isabelle_scala_script raises warnings (2 messages, latest: Nov 27 2023 at 09:13)
• [isabelle] jEdit vs. `isabelle server` timing differences. (3 messages, latest: Nov 26 2023 at 13:17)
• [isabelle] New in the AFP: Soundness of the Q0 proof syst... (1 message, latest: Nov 26 2023 at 10:32)
• [isabelle] New in the AFP: The Cardinality of the Continuum (1 message, latest: Nov 26 2023 at 10:24)
• [isabelle] 'Call for Papers: 17th Conference on Intellige... (1 message, latest: Nov 24 2023 at 07:42)
• [isabelle] New in the AFP: Myhill-Nerode Theorem for Nomi... (1 message, latest: Nov 23 2023 at 14:56)
• [isabelle] FMBC 2024 - First Call for Papers (1 message, latest: Nov 22 2023 at 13:01)
• [isabelle] New in the AFP: The Polylogarithm Function (1 message, latest: Nov 22 2023 at 09:56)
• [isabelle] New in the AFP: Critical points of a complex p... (1 message, latest: Nov 21 2023 at 14:54)
• [isabelle] New in the AFP: Chebyshev Polynomials (1 message, latest: Nov 21 2023 at 14:38)
• [isabelle] New in the AFP: Metatheory of Q0 (4 messages, latest: Nov 17 2023 at 16:53)
• [isabelle] New in the AFP: Labeled Transition Systems and... (1 message, latest: Nov 17 2023 at 10:03)
• [isabelle] POPL 2024 - Call for Participation - Early reg... (1 message, latest: Nov 13 2023 at 14:52)
• [isabelle] New in the AFP: Perfect Fields and Repeated Fa... (1 message, latest: Nov 13 2023 at 14:26)
• [isabelle] VerifyThis 2024 : Call for Problems (1 message, latest: Nov 09 2023 at 15:25)
• [isabelle] Monomorphisms and epimorphisms (5 messages, latest: Nov 09 2023 at 08:19)
• [isabelle] Globally disabling record syntax? (5 messages, latest: Nov 08 2023 at 14:02)
• [isabelle] Type arity declaration in Isabelle (5 messages, latest: Nov 08 2023 at 13:28)
• [isabelle] Postdoc position in Formal Methods at Universi... (2 messages, latest: Nov 08 2023 at 12:05)
• [isabelle] New in the AFP: The Disintegration Theorem (1 message, latest: Nov 07 2023 at 16:23)
• [isabelle] Large case distinctions in Isabelle (3 messages, latest: Nov 04 2023 at 15:26)
• [isabelle] Insufficiently general variable bindings from ... (5 messages, latest: Nov 04 2023 at 15:25)
• [isabelle] New in the AFP: Eudoxus Reals (2 messages, latest: Nov 04 2023 at 02:43)
• [isabelle] Missing indentation with LaTeX listings package (2 messages, latest: Nov 01 2023 at 15:18)
• [isabelle] sort-of bug in isabelle's "also..finally" (3 messages, latest: Oct 27 2023 at 12:20)
• [isabelle] POPL 2024 Student Research Competition - deadl... (1 message, latest: Oct 26 2023 at 20:12)
• [isabelle] Pattern ignored in simproc equality (6 messages, latest: Oct 26 2023 at 07:16)
• [isabelle] PriSC 2024: Call for Presentations (1 message, latest: Oct 25 2023 at 19:17)
• [isabelle] IJCAR 2024: call for co-located events (1 message, latest: Oct 25 2023 at 09:55)
• [isabelle] Post-doc job offering in SAT/SMT at Australian... (1 message, latest: Oct 25 2023 at 09:54)
• [isabelle] Postdoctoral Research Fellow (3 years) (1 message, latest: Oct 24 2023 at 12:16)
• [isabelle] cut for context_parser + improved error messag... (2 messages, latest: Oct 23 2023 at 12:27)
• [isabelle] [ICTAC 2023] Call for Participation (1 message, latest: Oct 22 2023 at 10:55)
• [isabelle] PhD or postdoc position in logical modelling o... (1 message, latest: Oct 19 2023 at 21:10)
• [isabelle] instantiation / enumeration for a type defined... (2 messages, latest: Oct 18 2023 at 23:26)
• [isabelle] CfP: Special issue on "Non-Classical Reasoning... (1 message, latest: Oct 18 2023 at 07:46)
• [isabelle] IJCAR 2024 --- Call for Papers (2 messages, latest: Oct 17 2023 at 20:40)
• [isabelle] NASA NFM 2024 (1 message, latest: Oct 17 2023 at 20:40)
• [isabelle] Missing session sources entry / source file er... (3 messages, latest: Oct 17 2023 at 15:54)
• [isabelle] New in the AFP: Hypergraph Colouring Bounds (1 message, latest: Oct 16 2023 at 14:30)
• [isabelle] (Extended Deadline) Dafny Workshop at POPL 24 (1 message, latest: Oct 16 2023 at 10:54)
• [isabelle] Trying to prove a property about a function wh... (2 messages, latest: Oct 16 2023 at 10:15)
• [isabelle] Transforming arithmetic expressions into polyn... (3 messages, latest: Oct 16 2023 at 10:08)
• [isabelle] POPL24 - Call for Student Volunteers (1 message, latest: Oct 14 2023 at 19:23)
• [isabelle] ACL2-2023 Second Call for Participation (1 message, latest: Oct 14 2023 at 19:23)
• [isabelle] LOPSTR 2023 - Final Call for Participation (2 messages, latest: Oct 13 2023 at 18:20)
• [isabelle] New in the AFP: Transport via Partial Galois C... (1 message, latest: Oct 13 2023 at 13:06)
• [isabelle] Dov Gabbay Prize 2023 - Online Ceremony (1 message, latest: Oct 13 2023 at 07:15)
• [isabelle] Preliminary CFP - FICS Workshop (submission de... (1 message, latest: Oct 12 2023 at 12:57)
• [isabelle] VSCode extension, notebooks and the web (7 messages, latest: Oct 12 2023 at 12:45)
• [isabelle] new in the AFP: Standard Borel Spaces (1 message, latest: Oct 11 2023 at 23:59)
• [isabelle] new in the AFP: S-Finite Measure Monad on Quas... (1 message, latest: Oct 11 2023 at 23:37)
• [isabelle] new in the AFP: Conformance Relations between ... (1 message, latest: Oct 11 2023 at 05:57)
• [isabelle] new in the AFP: Coupled Similarity and Contras... (1 message, latest: Oct 11 2023 at 05:40)
• [isabelle] New in the AFP: ML_Unification (3 messages, latest: Oct 10 2023 at 10:42)
• [isabelle] Permanent Academic posts for Early Career Rese... (1 message, latest: Oct 09 2023 at 12:38)
• [isabelle] What does it mean when a schematic variable is... (4 messages, latest: Oct 09 2023 at 11:43)
• [isabelle] VSCode extention for latest vscode version (23 messages, latest: Oct 04 2023 at 12:24)
• [isabelle] two small theories about the unit interval (3 messages, latest: Oct 03 2023 at 16:15)
• [isabelle] Status of automation for machine words (5 messages, latest: Sep 28 2023 at 14:05)
• [isabelle] Multiple theorem proving PhD/postdoc positions... (1 message, latest: Sep 28 2023 at 12:50)
• [isabelle] jEdit not opening on MacOS (7 messages, latest: Sep 28 2023 at 11:41)
• [isabelle] Permanent Post in Formal Methods at Swansea Un... (1 message, latest: Sep 28 2023 at 07:09)
• [isabelle] (2nd CfP) Dafny Workshop at POPL 24 (1 message, latest: Sep 27 2023 at 14:26)
• [isabelle] Call for Participation: VerifyThis Long-Term C... (1 message, latest: Sep 26 2023 at 12:28)
• [isabelle] New in the AFP: Cardinality and Representation... (1 message, latest: Sep 26 2023 at 10:32)
• [isabelle] 2nd Call for Papers Proceedings for ThEdu'23 -... (1 message, latest: Sep 26 2023 at 08:17)
• [isabelle] New in the AFP: Euler's Polyhedron Formula by ... (1 message, latest: Sep 22 2023 at 11:21)
• [isabelle] New in the AFP: "Hypergraphs" and "General Pro... (1 message, latest: Sep 22 2023 at 11:07)
• [isabelle] arithmetic modulo one (1 message, latest: Sep 21 2023 at 13:47)
• [isabelle] iFM 2023 call for participation (1 message, latest: Sep 21 2023 at 13:12)
• [isabelle] Default sidekick parser extension (1 message, latest: Sep 21 2023 at 13:12)
• [isabelle] "No content for theory certificate" for local ... (1 message, latest: Sep 21 2023 at 00:30)
• [isabelle] PPDP 2023 Call for Participation (1 message, latest: Sep 18 2023 at 09:59)
• [isabelle] FMCAD 2023: Call for Participation (1 message, latest: Sep 18 2023 at 05:20)
• [isabelle] ACL2-2023 Call for Participation (1 message, latest: Sep 17 2023 at 11:09)
• [isabelle] Phd position available (1 message, latest: Sep 14 2023 at 13:44)
• [isabelle] [CFP] PEPM at POPL 24 (1 message, latest: Sep 14 2023 at 13:44)
• [isabelle] Questions on Isabelle2023 (3 messages, latest: Sep 13 2023 at 21:26)
• [isabelle] new in AFP 2023: Directed Sets (1 message, latest: Sep 13 2023 at 14:51)
• [isabelle] AFP 2023 (1 message, latest: Sep 13 2023 at 14:30)
• [isabelle] Update of the AFP Entry "Actuarial_Mathematics" (1 message, latest: Sep 13 2023 at 12:36)
• [isabelle] Isabelle components unintuitive behaviour (4 messages, latest: Sep 12 2023 at 18:55)
• [isabelle] Plan for Isabelle2024 release (3 messages, latest: Sep 12 2023 at 18:41)
• [isabelle] Isabelle2023-RC3: Failure to recover from BibT... (2 messages, latest: Sep 12 2023 at 18:38)
• [isabelle] Announcing Isabelle2023 (1 message, latest: Sep 12 2023 at 16:56)
• [isabelle] ESOP 2024 Call For Papers (1 message, latest: Sep 12 2023 at 09:03)
• [isabelle] finite distribution (2 messages, latest: Sep 11 2023 at 13:24)
• [isabelle] Question about enumerable types (1 message, latest: Sep 10 2023 at 08:26)
• [isabelle] Question about enumerable types in Isabelle (2 messages, latest: Sep 09 2023 at 12:04)
• [isabelle] PhD Vacancy: Position on Verifying Quantum Pro... (1 message, latest: Sep 05 2023 at 20:19)
• [isabelle] Error "Tactic failed" in function definition (1 message, latest: Sep 05 2023 at 20:00)
• [isabelle] Isabelle2023-RC3: sledgehammer bug? (6 messages, latest: Sep 04 2023 at 08:30)
• [isabelle] smt failures on HOL-Analysis on Windows (14 messages, latest: Sep 04 2023 at 06:25)
• [isabelle] Last chance for testing: Isabelle2023-RC5 (1 message, latest: Sep 03 2023 at 19:09)
• [isabelle] Learning materials after Concrete Semantics? (1 message, latest: Sep 01 2023 at 17:27)
• [isabelle] Abduction Prover within Isabelle/HOL (2 messages, latest: Sep 01 2023 at 10:16)
• [isabelle] FSCD 2024: First Call for Papers (1 message, latest: Aug 31 2023 at 15:27)
• [isabelle] Workshop on Dafny at POPL 24 (Call for Papers) (1 message, latest: Aug 31 2023 at 12:43)
• [isabelle] wrong documentation in Isabelle/Isar Reference... (2 messages, latest: Aug 30 2023 at 15:12)
• [isabelle] ML Logger (4 messages, latest: Aug 30 2023 at 14:30)
• [isabelle] VMCAI 2024: Extended Deadline September 7th (1 message, latest: Aug 30 2023 at 10:25)
• [isabelle] Isabelle2023: Dependency on inetutils/hostname (5 messages, latest: Aug 28 2023 at 11:11)
• [isabelle] Isabelle2023-RC4 available for final testing (1 message, latest: Aug 27 2023 at 18:29)
• [isabelle] Four fully funded PhD positions (1 message, latest: Aug 26 2023 at 18:28)
• [isabelle] Research Associate at the University of Kent, ... (1 message, latest: Aug 21 2023 at 13:42)
• [isabelle] New in the AFP: Fixed-Length Vectors (3 messages, latest: Aug 21 2023 at 07:53)
• [isabelle] afp 2023 fork approaching (2 messages, latest: Aug 20 2023 at 13:45)
• [isabelle] New in the AFP: Ceva's Theorem (1 message, latest: Aug 18 2023 at 14:17)
• [isabelle] Is there any omega-cpo library in Isabelle (2 messages, latest: Aug 17 2023 at 19:44)
• [isabelle] VMCAI 2024: Second Call for Papers (1 message, latest: Aug 17 2023 at 09:40)
• [isabelle] new AFP entry: Catoids (1 message, latest: Aug 16 2023 at 17:20)
• [isabelle] Splitting with nested patterns (5 messages, latest: Aug 14 2023 at 15:50)
• [isabelle] Eisbach syntax specification to restrictive? (1 message, latest: Aug 14 2023 at 15:38)
• [isabelle] Isabelle/jEdit building workflow (6 messages, latest: Aug 14 2023 at 15:20)
• [isabelle] Isabelle2023-RC2: Sledgehammer prioritized ove... (11 messages, latest: Aug 11 2023 at 15:32)
• [isabelle] Isabelle/jEdit: Remote continuous proof checking (8 messages, latest: Aug 11 2023 at 09:50)
• [isabelle] New in the AFP: Polygonal_Number_Theorem (1 message, latest: Aug 11 2023 at 09:16)
• [isabelle] Isabelle2023-RC3 available for further testing (1 message, latest: Aug 10 2023 at 21:26)
• [isabelle] New in the AFP: Modal Quantales, Involutive Qu... (1 message, latest: Aug 10 2023 at 15:30)
• [isabelle] Corecursive definition not accepted (7 messages, latest: Aug 09 2023 at 21:22)
• [isabelle] Cartesian products of explicit sets do not sim... (3 messages, latest: Aug 09 2023 at 17:33)
• [isabelle] Locale interpretation and hidden polymorphism (4 messages, latest: Aug 09 2023 at 11:34)
• [isabelle] Isabelle2023-RC2: Proof state not shown after ... (5 messages, latest: Aug 08 2023 at 15:56)
• [isabelle] New in the AFP: Earley Parser (1 message, latest: Aug 08 2023 at 14:38)
• [isabelle] 2nd CFP - CPP 2024 - Certified Programs and Pr... (1 message, latest: Aug 08 2023 at 13:02)
• [isabelle] How to limit RAM usage of Poly/ML (4 messages, latest: Aug 08 2023 at 12:06)
• [isabelle] Isabelle2023-RC2: semantics of print_theorems ... (5 messages, latest: Aug 08 2023 at 10:42)
• [isabelle] [Call for submissions TFPiE 2024] Trends in Fu... (1 message, latest: Aug 08 2023 at 08:58)
• [isabelle] call for Associate Professor candidates in JAIST (1 message, latest: Aug 07 2023 at 10:53)
• [isabelle] Extended deadline: JSC special issue on the in... (1 message, latest: Aug 07 2023 at 05:53)
• [isabelle] PhD and PostDoc Positions in Formal Methods at... (1 message, latest: Aug 06 2023 at 20:55)
• [isabelle] Hints on "hg bisect" (1 message, latest: Aug 06 2023 at 14:15)
• [isabelle] FMBC 2024 - Preliminary CfP (1 message, latest: Aug 04 2023 at 15:15)
• [isabelle] Support for unicode character U+22D2 in the de... (1 message, latest: Aug 04 2023 at 12:42)
• [isabelle] Instantiating in rewrite method: bug or I don'... (4 messages, latest: Aug 03 2023 at 11:32)
• [isabelle] Nitpick hardcoded limit of 65536: (2 messages, latest: Aug 02 2023 at 08:21)
• [isabelle] Restrictions on the use of type variable names... (4 messages, latest: Jul 31 2023 at 07:30)
• [isabelle] POPL 2024 - Call for Tutorials (deadline: 15 O... (1 message, latest: Jul 28 2023 at 13:24)
• [isabelle] Isabelle2023-RC2: porting of Isabelle-LLVM wit... (2 messages, latest: Jul 27 2023 at 18:40)
• [isabelle] CICM 2023 - Call for Participation (1 message, latest: Jul 27 2023 at 09:49)
• [isabelle] Isabelle2023-RC1 - prints results only with "P... (3 messages, latest: Jul 26 2023 at 21:40)
• [isabelle] Isabelle2023-RC2 available for testing (1 message, latest: Jul 26 2023 at 21:30)
• [isabelle] Automatic theorem/definition printing appears ... (3 messages, latest: Jul 26 2023 at 14:40)
• [isabelle] VMCAI 2024: First Call for Papers (1 message, latest: Jul 26 2023 at 13:28)
• [isabelle] Two Postdoctoral Research Fellows at the Unive... (1 message, latest: Jul 20 2023 at 17:58)
• [isabelle] Reminder: EuroProofNet Workshops, Cambridge, ... (1 message, latest: Jul 19 2023 at 17:15)
• [isabelle] SBMF 2023 second call for papers (1 message, latest: Jul 19 2023 at 14:55)
• [isabelle] Isabelle2023-RC1 available for testing --- dea... (1 message, latest: Jul 18 2023 at 09:30)
• [isabelle] ThEdu'23 proceedings - cfp (1 message, latest: Jul 16 2023 at 20:59)
• [isabelle] FROM 2023 – THIRD CALL FOR PAPERS (1 message, latest: Jul 14 2023 at 10:14)
• [isabelle] CfPart Reliability, safety and security of rai... (1 message, latest: Jul 14 2023 at 10:14)
• [isabelle] ILDS Coq and Lean Autumn School 2023 – THIRD C... (1 message, latest: Jul 14 2023 at 10:13)
• [isabelle] [TFP 2024 Call for Papers] 25th International ... (1 message, latest: Jul 12 2023 at 15:17)
• [isabelle] Dov Gabbay Prize 2023 (1 message, latest: Jul 12 2023 at 05:36)
• [isabelle] Isabelle2023-RC1 available for testing (1 message, latest: Jul 11 2023 at 20:21)
• [isabelle] New in the AFP: Gray Codes for Arbitrary Numer... (1 message, latest: Jul 11 2023 at 17:24)
• [isabelle] SAC 2024: Call for Papers (1 message, latest: Jul 10 2023 at 17:27)
• [isabelle] Deadline Extension Doctoral Programme CICM 202... (1 message, latest: Jul 07 2023 at 06:40)
• [isabelle] Text-antiquotation: strange behavior (1 message, latest: Jul 06 2023 at 09:58)
• [isabelle] Announcement: EuroProofNet Workshops, Cambridg... (1 message, latest: Jul 04 2023 at 11:31)
• [isabelle] FMCAD 2023 Student Forum: Call for Contributions (1 message, latest: Jul 02 2023 at 21:34)
• [isabelle] Women in EuroProofNet @ ITP - Funding available (1 message, latest: Jul 02 2023 at 10:23)
• [isabelle] PhD Symposium iFM 2023 - Call for Papers [Dead... (1 message, latest: Jun 29 2023 at 15:12)
• [isabelle] New in the AFP: Executable Randomized Algorithms (1 message, latest: Jun 29 2023 at 10:46)
• [isabelle] 1st CFP - CPP 2024 - Certified Programs and Pr... (1 message, latest: Jun 27 2023 at 16:29)
• [isabelle] PhD student in Computing Science on safe and e... (1 message, latest: Jun 27 2023 at 12:03)
• [isabelle] POPL 2024: Final Call for Papers (1 message, latest: Jun 25 2023 at 13:46)
• [isabelle] new AFP entry: DCR Syntax and Execution Equiva... (1 message, latest: Jun 21 2023 at 05:41)
• [isabelle] CfP: FTSCS 2023: 9th ACM Workshop on Formal Te... (1 message, latest: Jun 14 2023 at 11:33)
• [isabelle] [ICTAC 2023] Final call for papers – New deadl... (1 message, latest: Jun 14 2023 at 11:33)
• [isabelle] The Decision Problem for Effective Procedures ... (1 message, latest: Jun 14 2023 at 11:32)
• [isabelle] new in the AFP: Zeckendorf’s Theorem (1 message, latest: Jun 14 2023 at 11:05)
• [isabelle] New in the AFP: Cryptographic Standards (1 message, latest: Jun 13 2023 at 12:48)
• [isabelle] Meeting IFIP WG 1.6 on Rewriting (5 July 2023)... (1 message, latest: Jun 11 2023 at 15:03)
• [isabelle] New in the AFP: Inner Structure, Determinism a... (1 message, latest: Jun 09 2023 at 10:04)
• [isabelle] Isabelle2023-RC0: ML heap size has been signif... (1 message, latest: Jun 07 2023 at 19:20)
• [isabelle] Isabelle2023-RC0 available as preview for expe... (1 message, latest: Jun 07 2023 at 18:58)
• [isabelle] DC@KI2023: Doctoral Consortium at KI 2023 - CfP (1 message, latest: Jun 06 2023 at 18:33)
• [isabelle] POPL 2024: Call for Workshops and Co-located E... (1 message, latest: Jun 06 2023 at 18:33)
• [isabelle] Call for Participation -- LFMTP 2023 (1 message, latest: Jun 04 2023 at 11:35)
• [isabelle] New in the AFP: A Verified Efficient Implement... (1 message, latest: Jun 01 2023 at 23:04)
• [isabelle] ITP 2023 Call for Participation (1 message, latest: Jun 01 2023 at 13:34)
• [isabelle] HOR 2023: Call for Participation (1 message, latest: May 31 2023 at 13:30)
• [isabelle] PhD Symposium iFM 2023 - Call for Papers (2 messages, latest: May 30 2023 at 15:52)
• [isabelle] UNIF 2023 Call for Participation (1 message, latest: May 29 2023 at 07:52)
• [isabelle] Isabelle/UTP and CyPhyAssure tools for Isabelle (2 messages, latest: May 25 2023 at 13:08)
• [isabelle] Building fork releases (5 messages, latest: May 23 2023 at 19:38)
• [isabelle] PDF document output: theory documents are empty (1 message, latest: May 23 2023 at 11:12)
• [isabelle] Postdoctoral position at Université de Montpel... (1 message, latest: May 22 2023 at 15:34)
• [isabelle] FSCD 2023: Call for Participation (early regis... (1 message, latest: May 19 2023 at 13:01)
• [isabelle] 2nd Call for Papers: 19th International Worksh... (1 message, latest: May 19 2023 at 10:56)
• [isabelle] New in the AFP: MLSS Decision Procedure (1 message, latest: May 18 2023 at 13:27)
• [isabelle] Inconsistent behaviour between Isabelle/HOL in... (4 messages, latest: May 17 2023 at 18:22)
• [isabelle] Deduktionstreffen 2023 - Call for contributions (1 message, latest: May 17 2023 at 15:18)
• [isabelle] New in the AFP: Tree Enumeration (2 messages, latest: May 17 2023 at 11:37)
• [isabelle] New in the AFP: The CHSH inequality: Tsirelson... (1 message, latest: May 17 2023 at 10:01)
• [isabelle] New in the AFP: the Three Squares Theorem (1 message, latest: May 16 2023 at 14:47)
• [isabelle] CADE-29: Call for participation (1 message, latest: May 15 2023 at 14:05)
• [isabelle] [fm-announcements] FMICS 2023 - Deadline exten... (1 message, latest: May 15 2023 at 14:04)
• [isabelle] Locale interpretation and code generation (2 messages, latest: May 11 2023 at 08:28)
• [isabelle] LOPSTR 2023 (Lisbon) - Final Call for Papers -... (1 message, latest: May 10 2023 at 09:53)
• [isabelle] Duplicate Fact Declaration Because of Name Man... (2 messages, latest: May 10 2023 at 07:47)
• [isabelle] New in the AFP: The Halting Problem Is Soluble... (1 message, latest: May 10 2023 at 01:37)
• [isabelle] TABLEAUX 2023 - FINAL CALL FOR PAPERS (DEADLIN... (1 message, latest: May 09 2023 at 20:48)
• [isabelle] Call for Proposals: EuroProofNet – Short-Term ... (1 message, latest: May 05 2023 at 13:32)
• [isabelle] CfP: JSC special issue on the interaction of S... (1 message, latest: May 04 2023 at 09:38)
• [isabelle] HOR 2023: Final Call for Papers (extended dead... (1 message, latest: May 04 2023 at 09:03)
• [isabelle] Persisting proof data in theory (7 messages, latest: May 03 2023 at 20:31)
• [isabelle] New in the AFP: The Schwartz-Zippel Lemma (1 message, latest: May 03 2023 at 13:11)
• [isabelle] CfP RSSRail 2023 - extended submission deadline (1 message, latest: May 03 2023 at 10:58)
• [isabelle] FMCAD 2023: Final Call for Papers with *** Dea... (1 message, latest: May 02 2023 at 07:30)
• [isabelle] Heavy memory use with sledgehammer (25 messages, latest: May 02 2023 at 00:28)
• [isabelle] Call for Papers -- Formal Techniques for Java-... (1 message, latest: Apr 30 2023 at 10:13)
• [isabelle] Removing type class instances? (3 messages, latest: Apr 28 2023 at 23:55)
• [isabelle] AITP 2023 - Second Call for Contributions (1 message, latest: Apr 28 2023 at 10:06)
• [isabelle] External prover crashing with SIGABRT (was: He... (5 messages, latest: Apr 27 2023 at 21:14)
• [isabelle] \<bbbA> (2 messages, latest: Apr 27 2023 at 09:23)
• [isabelle] POPL 2024: Call for Papers (deadline: July 11) (1 message, latest: Apr 26 2023 at 10:06)
• [isabelle] Long-names and parse_term (3 messages, latest: Apr 24 2023 at 14:58)
• [isabelle] Final CfP: Logical and Semantic Frameworks wit... (1 message, latest: Apr 23 2023 at 14:25)
• [isabelle] WiL 2023: Call for contributions (1 message, latest: Apr 23 2023 at 14:24)
• [isabelle] CfP LSFA 2023: extended deadlines (1 message, latest: Apr 23 2023 at 08:37)
• [isabelle] New in the AFP: A Formalization of the SCL(FOL... (1 message, latest: Apr 22 2023 at 03:25)
• [isabelle] Summer School "Interactions of Proof Assistant... (1 message, latest: Apr 21 2023 at 13:50)
• [isabelle] HOR 2023: Second Call for Papers (1 message, latest: Apr 21 2023 at 11:42)
• [isabelle] Call for Papers: 19th International Workshop o... (1 message, latest: Apr 20 2023 at 15:01)
• [isabelle] PPDP 2023 - Call for Papers (1 message, latest: Apr 20 2023 at 15:01)
• [isabelle] 3-year Research Associate or Research Assistan... (1 message, latest: Apr 20 2023 at 11:11)
• [isabelle] LSFA 2023: 2nd CfP (1 message, latest: Apr 18 2023 at 08:31)
• [isabelle] New in the AFP: Formalization of Hyper Hoare L... (1 message, latest: Apr 18 2023 at 03:36)
• [isabelle] 4y fully funded PhD position on verification o... (2 messages, latest: Apr 17 2023 at 11:45)
• [isabelle] The partial_function command (3 messages, latest: Apr 17 2023 at 11:12)
• [isabelle] WLOG in Isabelle/HOL (14 messages, latest: Apr 17 2023 at 08:43)
• [isabelle] LOPSTR 2023 (Lisbon) - Second Call for Papers ... (1 message, latest: Apr 16 2023 at 09:39)
• [isabelle] HOLCF conversions to set (2 messages, latest: Apr 14 2023 at 19:22)
• [isabelle] New in the AFP: Positional Notation for Natura... (1 message, latest: Apr 14 2023 at 13:36)
• [isabelle] Last Call for Participation (Deadline April 17... (1 message, latest: Apr 13 2023 at 08:48)
• [isabelle] Final Call for Papers LFMTP'23 [extended abstr... (1 message, latest: Apr 12 2023 at 13:46)
• [isabelle] Invitation to participate in an AI mathematica... (1 message, latest: Apr 12 2023 at 10:40)
• [isabelle] Rule works, intro fails (4 messages, latest: Apr 11 2023 at 14:22)
• [isabelle] [fm-announcements] FMICS 2023 - Second call fo... (1 message, latest: Apr 10 2023 at 17:10)
• [isabelle] New in the AFP: Distributed Distinct Elements (1 message, latest: Apr 06 2023 at 11:43)
• [isabelle] New in the AFP: Formalization of CommCSL by Th... (1 message, latest: Apr 04 2023 at 12:02)
• [isabelle] Final Call for Papers: Logical Frameworks and ... (1 message, latest: Apr 03 2023 at 10:34)
• [isabelle] IFL23 first CFP (1 message, latest: Apr 03 2023 at 10:34)
• [isabelle] Postdoc position on design and/or verification... (2 messages, latest: Apr 03 2023 at 09:28)
• [isabelle] Two Open Positions (Senior Research Associate)... (1 message, latest: Mar 31 2023 at 12:47)
• [isabelle] Spacing in Isabelle documents (1 message, latest: Mar 31 2023 at 08:19)
• [isabelle] Encoding of contributors file (2 messages, latest: Mar 29 2023 at 20:46)
• [isabelle] Isar Virtual Machine (1 message, latest: Mar 29 2023 at 15:07)
• [isabelle] Sledgehammer (2 messages, latest: Mar 29 2023 at 10:38)
• [isabelle] CICM 2023, Extended deadlines 3.4.2023 (abstra... (1 message, latest: Mar 29 2023 at 09:14)
• [isabelle] CFP: 14th International Workshop on the Implem... (1 message, latest: Mar 28 2023 at 11:22)
• [isabelle] FMCAD 2023: Second Call for Papers (1 message, latest: Mar 28 2023 at 07:54)
• [isabelle] New in the AFP: No Faster-Than-Light Observers... (1 message, latest: Mar 27 2023 at 16:38)
• [isabelle] VerifyThis 2023: Call For Participation (1 message, latest: Mar 24 2023 at 10:48)
• [isabelle] SAS 2023 - First Call for Papers - Paper Deadl... (1 message, latest: Mar 21 2023 at 14:53)
• [isabelle] PPDP 2023 - Preliminary Call for Papers (1 message, latest: Mar 19 2023 at 10:49)
• [isabelle] TABLEAUX 2023 - FIRST CALL FOR PAPERS (1 message, latest: Mar 18 2023 at 13:30)
• [isabelle] New in the AFP: Expander Graphs by Emin Karayel (1 message, latest: Mar 17 2023 at 10:04)
• [isabelle] ITP 2023: Call for Workshop and Tutorial Propo... (1 message, latest: Mar 16 2023 at 15:04)
• [isabelle] New in the AFP: "Intersection of two monoids g... (1 message, latest: Mar 16 2023 at 15:04)
• [isabelle] Debugging a hanging Isabelle build (7 messages, latest: Mar 15 2023 at 14:54)
• [isabelle] LPAR 2023 Deadline extension (1 message, latest: Mar 14 2023 at 23:02)
• [isabelle] Gracefully disabling SystemOnTPTP broadcast fo... (3 messages, latest: Mar 13 2023 at 19:07)
• [isabelle] AFP Word_Lib: strange lemma names (4 messages, latest: Mar 13 2023 at 15:02)
• [isabelle] LOPSTR 2023 - Call for Papers (1 message, latest: Mar 12 2023 at 12:01)
• [isabelle] cfp ThEdu'23 -- 12th workshop on theorem provi... (2 messages, latest: Mar 11 2023 at 15:42)
• [isabelle] Lectureships at Lancaster University (Leipzig ... (1 message, latest: Mar 10 2023 at 14:58)
• [isabelle] PhD and Post-doc Positions in Computer Science... (1 message, latest: Mar 10 2023 at 09:31)
• [isabelle] PhD or Postdoc Position at LMU Munich about Ve... (1 message, latest: Mar 10 2023 at 00:08)
• [isabelle] ITP 2024 - Call for Bids (1 message, latest: Mar 09 2023 at 18:07)
• [isabelle] Apparent dovetailing/scheduling problem with S... (10 messages, latest: Mar 09 2023 at 10:09)
• [isabelle] iFM 2023 - Call for Papers (1 message, latest: Mar 08 2023 at 18:15)
• [isabelle] OPLSS 2023: Summer School Dates (1 message, latest: Mar 08 2023 at 17:38)
• [isabelle] Call for papers SC-square 2023 (1 message, latest: Mar 08 2023 at 17:37)
• [isabelle] UNIF 2023 Second Call for Papers (1 message, latest: Mar 08 2023 at 17:37)
• [isabelle] TYPES 2023: Call for Contributions - Deadline ... (1 message, latest: Mar 08 2023 at 17:37)
• [isabelle] LSFA 2023: 1st CfP (1 message, latest: Mar 07 2023 at 17:25)
• [isabelle] Performance drop after `no_notation` (3 messages, latest: Mar 07 2023 at 15:59)
• [isabelle] Announce: Summer School about the use of Proof... (1 message, latest: Mar 07 2023 at 13:44)
• [isabelle] New in the AFP: A Sound and Complete Calculus ... (1 message, latest: Mar 07 2023 at 13:02)
• [isabelle] PhD Studentships in Formalising CS/Maths at Ki... (1 message, latest: Mar 06 2023 at 12:38)
• [isabelle] FMCAD 2023: First Call for Papers (1 message, latest: Mar 06 2023 at 05:23)
• [isabelle] CALCO 2023: Deadline Extension (1 message, latest: Mar 05 2023 at 14:46)
• [isabelle] CfP Reliability, safety and security of railwa... (1 message, latest: Mar 02 2023 at 15:17)
• [isabelle] Second Call for Papers: Logical Frameworks and... (1 message, latest: Mar 02 2023 at 15:16)
• [isabelle] New in the AFP: Renaming-Enriched Sets (Renset... (1 message, latest: Mar 02 2023 at 14:09)
• [isabelle] Question on proof of a lemma (1 message, latest: Mar 02 2023 at 13:23)
• [isabelle] AITP 2023 - Call for Contributions (1 message, latest: Mar 02 2023 at 09:03)
• [isabelle] New in the AFP: Group Law of Edwards Elliptic ... (1 message, latest: Mar 01 2023 at 16:21)
• [isabelle] print_record command and extensible record type (1 message, latest: Feb 27 2023 at 11:31)
• [isabelle] Bypass PIDE error Bad name: "__"⌂ (3 messages, latest: Feb 27 2023 at 11:30)
• [isabelle] HOR 2023: Call for Papers (1 message, latest: Feb 27 2023 at 10:07)
• [isabelle] CALCO 2023: Final Call for Papers (1 message, latest: Feb 23 2023 at 17:30)
• [isabelle] [ICTAC 2023] First call for papers – deadline ... (1 message, latest: Feb 23 2023 at 11:42)
• [isabelle] 1st Call for Contributions - Women in Logic Wo... (1 message, latest: Feb 23 2023 at 11:42)
• [isabelle] CADE-29 - Second Call for Papers (1 message, latest: Feb 22 2023 at 15:03)
• [isabelle] Syntax in Map.thy (7 messages, latest: Feb 21 2023 at 14:40)
• [isabelle] Quanta Magazine article on an LLM for Isabelle (3 messages, latest: Feb 20 2023 at 07:06)
• [isabelle] 2nd Call for Papers, Conference on Intelligent... (1 message, latest: Feb 19 2023 at 11:22)
• [isabelle] metis blindspot? (1 message, latest: Feb 18 2023 at 19:22)
• [isabelle] CFP: LPAR-24 (Logic for Programming, Artificia... (1 message, latest: Feb 17 2023 at 21:01)
• [isabelle] FSCD 2025: Call for Location (1 message, latest: Feb 17 2023 at 11:14)
• [isabelle] Prime number theorem with classical remainder ... (2 messages, latest: Feb 16 2023 at 15:36)
• [isabelle] Hilbert Basis Theorem? (2 messages, latest: Feb 15 2023 at 10:52)
• [isabelle] Sledgehammer reconstructions fail (+ irregular... (6 messages, latest: Feb 14 2023 at 13:01)
• [isabelle] TYPES 2023 - Call for Contributions (1 message, latest: Feb 13 2023 at 16:48)
• [isabelle] TABLEAUX 2023 - PRELIMINARY CALL FOR PAPERS (1 message, latest: Feb 13 2023 at 04:24)
• [isabelle] Bug report: problem with (too trivial?) abbrev... (6 messages, latest: Feb 12 2023 at 18:37)
• [isabelle] Isabelle:Output window in VSCodium (2 messages, latest: Feb 08 2023 at 20:51)
• [isabelle] The link to the User Mailinglist Archive is se... (3 messages, latest: Feb 07 2023 at 13:04)
• [isabelle] chatgpt and Isabelle/HOL4? :) (5 messages, latest: Feb 07 2023 at 08:41)
• [isabelle] New in the AFP: Hardness of Lattice Problems b... (1 message, latest: Feb 06 2023 at 07:26)
• [isabelle] New in the AFP: ABY3 Multiplication and Array ... (1 message, latest: Feb 05 2023 at 11:07)
• [isabelle] CALCO 2023: Second Call for Papers (1 message, latest: Feb 03 2023 at 17:46)
• [isabelle] Side-effect of subset_antisym [intro! (1 message, latest: Feb 03 2023 at 10:46)
• [isabelle] Global interpretation and theory import diamond (3 messages, latest: Feb 02 2023 at 08:36)
• [isabelle] Working remotely (1 message, latest: Feb 01 2023 at 14:58)
• [isabelle] SMC-IT and SCC Deadline Extension (March 3rd 2... (1 message, latest: Feb 01 2023 at 14:51)
• [isabelle] [fm-announcements] FMICS 2023 - Call for Papers (1 message, latest: Feb 01 2023 at 14:51)
• [isabelle] FSCD 2023: Extended deadline (Abstract: Februa... (1 message, latest: Feb 01 2023 at 10:07)
• [isabelle] New in the AFP: Given Clause Loops (1 message, latest: Jan 31 2023 at 15:59)
• [isabelle] lattice_syntax by default? (3 messages, latest: Jan 25 2023 at 07:04)
• [isabelle] New in the AFP: Suppes' Theorem for Probabilit... (1 message, latest: Jan 25 2023 at 06:38)
• [isabelle] Job offer / Researcher-Engineer / Inria, Sacla... (1 message, latest: Jan 24 2023 at 13:46)
• [isabelle] Open Position: Assistant Professor with Specia... (1 message, latest: Jan 23 2023 at 20:35)
• [isabelle] New in the AFP: A Hoare Logic for Diverging Pr... (1 message, latest: Jan 22 2023 at 23:34)
• [isabelle] Pattern matching on extended records (1 message, latest: Jan 20 2023 at 15:29)
• [isabelle] ITP 2023: Second Call for Papers (1 message, latest: Jan 20 2023 at 12:20)
• [isabelle] Using Isar methods from ML (6 messages, latest: Jan 19 2023 at 01:20)
• [isabelle] Another limitation of HOL: Binding the type va... (1 message, latest: Jan 18 2023 at 21:50)
• [isabelle] Suggestions for new formalizations on mathemat... (10 messages, latest: Jan 18 2023 at 16:37)
• [isabelle] What is the meaning of the parameter syntax an... (2 messages, latest: Jan 18 2023 at 16:35)
• [isabelle] FSCD 2023: Second Call for Papers (1 message, latest: Jan 18 2023 at 16:16)
• [isabelle] New in the AFP: Strict Omega Categories (1 message, latest: Jan 16 2023 at 13:12)
• [isabelle] UNIF 2023 Call for Papers (1 message, latest: Jan 15 2023 at 15:41)
• [isabelle] Call for Papers: Logical Frameworks and Meta-L... (1 message, latest: Jan 15 2023 at 15:41)
• [isabelle] New coauthor for your chapter? (3 messages, latest: Jan 13 2023 at 16:29)
• [isabelle] CADE-29 - Call for Papers (1 message, latest: Jan 12 2023 at 12:47)
• [isabelle] New in the AFP: Abstract Object Theory (1 message, latest: Jan 12 2023 at 12:46)
• [isabelle] New in the AFP: Class-Based Classical Proposit... (1 message, latest: Jan 11 2023 at 15:03)
• [isabelle] FM 2023 - Call for Participation (1 message, latest: Jan 11 2023 at 10:44)
• [isabelle] coinduction proof goals (1 message, latest: Jan 11 2023 at 10:44)
• [isabelle] New in the AFP: The Cook-Levin Theorem (1 message, latest: Jan 10 2023 at 16:48)
• [isabelle] New in the AFP: Automation of Boolos' Curious ... (1 message, latest: Jan 10 2023 at 14:50)
• [isabelle] New in the AFP: Synthetic Completeness (1 message, latest: Jan 10 2023 at 11:38)
• [isabelle] Multi-dependence in Locale (2 messages, latest: Jan 09 2023 at 21:53)
• [isabelle] coinduction proof method (3 messages, latest: Jan 09 2023 at 17:27)
• [isabelle] (Infinite) Cardinalities of Datatypes (3 messages, latest: Jan 09 2023 at 16:48)
• [isabelle] Verification Jobs @ Cryspen (1 message, latest: Jan 08 2023 at 15:50)
• [isabelle] 2-year postdoctoral position in Neurosymbolic ... (1 message, latest: Jan 08 2023 at 15:50)
• [isabelle] How to enter special symbols with Isabelle/VSCode (1 message, latest: Jan 05 2023 at 02:33)
• [isabelle] Post-doc position at Université de Montpellier (1 message, latest: Jan 03 2023 at 11:11)
• [isabelle] [TFP 2023 Call For Participation] 24th Interna... (1 message, latest: Jan 02 2023 at 15:36)
• [isabelle] A fully funded postdoc position in "Quantitati... (1 message, latest: Jan 02 2023 at 11:00)
• [isabelle] Isabelle2022 document preparation: Inconsisten... (1 message, latest: Dec 31 2022 at 13:10)
• [isabelle] Quotient_type and locale (2 messages, latest: Dec 31 2022 at 09:19)
• [isabelle] Using Types_To_Sets (19 messages, latest: Dec 29 2022 at 22:14)
• [isabelle] Exporting proof terms out of Isabelle (3 messages, latest: Dec 27 2022 at 09:59)
• [isabelle] Proofterms reification function to the metalogic (7 messages, latest: Dec 27 2022 at 08:50)
• [isabelle] Third Call for Papers ABZ 2023 (Nancy, Lorrain... (1 message, latest: Dec 23 2022 at 22:39)
• [isabelle] Strange lemma HOL-Computational_Algebra/Primes... (1 message, latest: Dec 22 2022 at 12:31)
• [isabelle] Multiset leaves lifting setup open (6 messages, latest: Dec 21 2022 at 16:36)
• [isabelle] ITP Isabelle error (3 messages, latest: Dec 20 2022 at 14:14)
• [isabelle] Linear arithmetic should have refuted the assu... (1 message, latest: Dec 20 2022 at 13:52)
• [isabelle] CALCO 2023: First Call for Papers (1 message, latest: Dec 19 2022 at 17:55)
• [isabelle] Call for Workshops: Conference on Intelligent ... (2 messages, latest: Dec 17 2022 at 08:46)
• [isabelle] Call for Papers: Conference on Intelligent Com... (1 message, latest: Dec 17 2022 at 08:37)
• [isabelle] New in the AFP: A First Complete Algorithm for... (1 message, latest: Dec 16 2022 at 14:48)
• [isabelle] Some facts are not available in the int context (1 message, latest: Dec 16 2022 at 10:55)
• [isabelle] Duplicate fact declaration when interpreting l... (3 messages, latest: Dec 11 2022 at 15:05)
• [isabelle] Certified Programs and Proofs (CPP) 2023: Call... (1 message, latest: Dec 10 2022 at 10:42)
• [isabelle] NFM 2023: Deadline extension & final CFP (1 message, latest: Dec 10 2022 at 03:35)
• [isabelle] Auto-indenter and "subgoal" (3 messages, latest: Dec 06 2022 at 08:21)
• [isabelle] New in the AFP: Birkhoff's Representation Theo... (1 message, latest: Dec 06 2022 at 08:16)
• [isabelle] Opening for assistant professors w/tenure trac... (1 message, latest: Dec 05 2022 at 13:40)
• [isabelle] TFPIE 2023 call for submissions (deadline Dec ... (2 messages, latest: Dec 03 2022 at 23:29)
• [isabelle] new AFP entry: A Verified Translation of Multi... (1 message, latest: Dec 01 2022 at 21:38)
• [isabelle] New in the AFP: Kneser's Theorem and the Cauch... (1 message, latest: Dec 01 2022 at 13:37)
• [isabelle] New in the AFP: Turán's Graph Theorem (1 message, latest: Dec 01 2022 at 13:35)
• [isabelle] Announcing The Isabelle Cabal (1 message, latest: Dec 01 2022 at 09:58)
• [isabelle] FSCD-CADE 2023: Call for Workshop Proposals (1 message, latest: Nov 29 2022 at 11:59)
• [isabelle] FSCD 2023: First Call for Papers (1 message, latest: Nov 28 2022 at 20:15)
• [isabelle] New in the AFP: the Sauer-Shelah Lemma (1 message, latest: Nov 28 2022 at 16:43)
• [isabelle] New in the AFP: A Formal CHERI-C Memory Model (1 message, latest: Nov 28 2022 at 12:50)
• [isabelle] More Debug Info in Batch Build (3 messages, latest: Nov 25 2022 at 20:57)
• [isabelle] Code generation failing with lift_definition (3 messages, latest: Nov 23 2022 at 12:39)
• [isabelle] lemma top_empty_eq should not have attribute p... (1 message, latest: Nov 22 2022 at 14:06)
• [isabelle] State-of-the-art for code generation for funct... (5 messages, latest: Nov 21 2022 at 16:34)
• [isabelle] Proper IDE for Isabelle/Scala development (2 messages, latest: Nov 21 2022 at 12:51)
• [isabelle] Bezout equation for nat (1 message, latest: Nov 21 2022 at 12:19)
• [isabelle] Hiring 2 PhD students! (1 message, latest: Nov 21 2022 at 12:16)
• [isabelle] Call for Papers: NASA Formal Methods (NFM) 2023 (1 message, latest: Nov 18 2022 at 15:15)
• [isabelle] New in the AFP: The Incompatibility of Strateg... (1 message, latest: Nov 18 2022 at 10:08)
• [isabelle] ITP 2023: First Call for Papers (1 message, latest: Nov 17 2022 at 08:01)
• [isabelle] thm_oracles does not mention "sorry" when usin... (1 message, latest: Nov 16 2022 at 19:31)
• [isabelle] New in the AFP: The Balog–Szemerédi–Gowers The... (1 message, latest: Nov 16 2022 at 15:24)
• [isabelle] [TFP 2023 2nd Call for Papers] 24th Internatio... (1 message, latest: Nov 15 2022 at 09:32)
• [isabelle] Sam Staton giving this year's LMS/BCS-FACS Eve... (1 message, latest: Nov 14 2022 at 12:50)
• [isabelle] New in the AFP: Combinatorial Enumeration Algo... (1 message, latest: Nov 14 2022 at 10:46)
• [isabelle] Items displayed in Sidekick (3 messages, latest: Nov 13 2022 at 17:38)
• [isabelle] Isabelle2022 leaking minisat processes (6 messages, latest: Nov 10 2022 at 10:51)
• [isabelle] Isabelle proof document outline contains oops'... (3 messages, latest: Nov 07 2022 at 15:01)
• [isabelle] Extended Deadline 11 November 2022 - Formal Me... (1 message, latest: Nov 04 2022 at 08:19)
• [isabelle] Error: Could not find or load main class isabe... (4 messages, latest: Nov 03 2022 at 11:28)
• [isabelle] VerifyThis 2023: Call For Problems (1 message, latest: Nov 02 2022 at 15:27)
• [isabelle] Postdoc position at the University of Birmingham (2 messages, latest: Nov 01 2022 at 16:53)
• [isabelle] Error of installing isabelle-linter in Isabell... (3 messages, latest: Oct 30 2022 at 09:30)
• [isabelle] CIE 2023: Batumi, Georgia July 24-28, 2023 (1 message, latest: Oct 30 2022 at 05:32)
• [isabelle] Instantiating a lemma with each case of an ind... (1 message, latest: Oct 29 2022 at 13:22)
• [isabelle] UTF-8 versus UTF-8-isabelle (9 messages, latest: Oct 28 2022 at 15:07)
• [isabelle] AFP 2022 (2 messages, latest: Oct 28 2022 at 11:09)
• [isabelle] 5th edition of the World Logic Day - January 1... (1 message, latest: Oct 28 2022 at 10:00)
• [isabelle] JVM options (6 messages, latest: Oct 26 2022 at 19:01)
• [isabelle] Testing Windows 11 (3 messages, latest: Oct 26 2022 at 14:58)
• [isabelle] PLAS 2022: Call for Papers (1 message, latest: Oct 26 2022 at 13:56)
• [isabelle] Isabelle2022 on macOS Ventura (1 message, latest: Oct 26 2022 at 09:31)
• [isabelle] Access to "old" versions of Isabelle ? (6 messages, latest: Oct 26 2022 at 08:09)
• [isabelle] CfP: Doctoral Symposium @ FM 2023 (1 message, latest: Oct 25 2022 at 19:16)
• [isabelle] Isabelle download in Windows 10 (13 messages, latest: Oct 20 2022 at 21:43)
• [isabelle] unsuscribe (1 message, latest: Oct 20 2022 at 10:28)
• [isabelle] Affine n-dimensional transformations ? (2 messages, latest: Oct 19 2022 at 08:53)
• [isabelle] isabelle server: purge theories not doing anyt... (3 messages, latest: Oct 18 2022 at 13:54)
• [isabelle] Final CFP: Proceedings for ThEdu'22 (1 message, latest: Oct 18 2022 at 12:35)
• [isabelle] Pre-final Isabelle2022-RC4 is now available (1 message, latest: Oct 18 2022 at 12:14)
• [isabelle] Is Sergeyev's grossone theory formalized in Is... (2 messages, latest: Oct 18 2022 at 09:46)
• [isabelle] Isabelle2022-RC3: isabelle scala in a path wit... (7 messages, latest: Oct 18 2022 at 08:48)
• [isabelle] Error : Naproche-SAD server failure (4 messages, latest: Oct 17 2022 at 21:36)
• [isabelle] FSEN 2023 final CfP: deadline extension and hy... (1 message, latest: Oct 17 2022 at 10:03)
• [isabelle] [Afp-submit] AFP devel links redirect to stable (1 message, latest: Oct 17 2022 at 08:59)
• [isabelle] AFP devel links redirect to stable (2 messages, latest: Oct 17 2022 at 08:44)
• [isabelle] Some basics about List.rotate1 (3 messages, latest: Oct 14 2022 at 16:09)
• [isabelle] Inconsistent parsing and highlighting of bound... (1 message, latest: Oct 14 2022 at 14:59)
• [isabelle] Anomaly in the “induction” method (3 messages, latest: Oct 14 2022 at 10:09)
• [isabelle] lifting and records (3 messages, latest: Oct 13 2022 at 12:14)
• [isabelle] Optional depth arguments in auto (4 messages, latest: Oct 13 2022 at 09:53)
• [isabelle] Suggestions for src/HOL/Fun.thy (4 messages, latest: Oct 12 2022 at 05:54)
• [isabelle] Reference for »canonical« definition of signed... (9 messages, latest: Oct 11 2022 at 17:44)
• [isabelle] Postdoc positions at Virginia Tech/Open Univer... (1 message, latest: Oct 10 2022 at 04:17)
• [isabelle] Isabelle2022-RC2: Where's signed_division *syn... (6 messages, latest: Oct 06 2022 at 12:28)
• [isabelle] LaTeX issue with \isasymlonglonglongrightarrow (2 messages, latest: Oct 06 2022 at 09:54)
• [isabelle] new AFP entry: Verification of Query Optimizat... (1 message, latest: Oct 05 2022 at 17:48)
• [isabelle] Missing lemma in `List` theory (2 messages, latest: Oct 05 2022 at 06:09)
• [isabelle] Two positions at the University of Bonn in the... (1 message, latest: Oct 04 2022 at 15:28)
• [isabelle] Assistant/Associate Professor in Logical Found... (1 message, latest: Oct 04 2022 at 12:53)
• [isabelle] Faculty positions in Oxford (1 message, latest: Oct 03 2022 at 09:57)
• [isabelle] release fork for afp-2022 (3 messages, latest: Oct 03 2022 at 09:03)
• [isabelle] Isabelle2022-RC3 available for final stage of ... (1 message, latest: Oct 02 2022 at 18:35)
• [isabelle] Call for Presentations: PriSC 2023 @ POPL 2023 (1 message, latest: Oct 02 2022 at 16:55)
• [isabelle] new AFP entry: Undirected Graph Theory (1 message, latest: Oct 01 2022 at 08:54)
• [isabelle] New in the AFP: Maximum Segment Sum (1 message, latest: Sep 30 2022 at 20:38)
• [isabelle] stronger Bzout theorem for natural numbers (2 messages, latest: Sep 30 2022 at 09:12)
• [isabelle] Isabelle2022-RC2 available for serious testing (3 messages, latest: Sep 30 2022 at 06:44)
• [isabelle] Fully funded PhD positions in logic, semantics... (1 message, latest: Sep 29 2022 at 11:13)
• [isabelle] New in the AFP: Making Arbitrary Relational Ca... (1 message, latest: Sep 29 2022 at 08:33)
• [isabelle] CIAC 2023 CFP (1 message, latest: Sep 29 2022 at 04:41)
• [isabelle] ProLaLa 2023 -- Programming Languages and the ... (1 message, latest: Sep 26 2022 at 16:03)
• [isabelle] [FSEN 2023] Second Call for Papers FSEN 2023 (1 message, latest: Sep 26 2022 at 15:49)
• [isabelle] New in the AFP: Stalnaker Logic (1 message, latest: Sep 26 2022 at 10:07)
• [isabelle] PLMW@POPL 2023: Call For Scholarship Applicati... (1 message, latest: Sep 23 2022 at 16:01)
• [isabelle] Mysteries of locales, "TYPE(T)", and "T itself" (5 messages, latest: Sep 22 2022 at 21:47)
• [isabelle] New in the AFP: p-Adic Fields and p-Adic Semia... (1 message, latest: Sep 22 2022 at 16:35)
• [isabelle] New in the AFP: Risk-Free Lending (1 message, latest: Sep 22 2022 at 15:19)
• [isabelle] 1st Call for Papers: NASA Formal Methods (NFM)... (1 message, latest: Sep 21 2022 at 00:52)
• [isabelle] Colorful Latex Document Preparation in 2022 (1 message, latest: Sep 20 2022 at 07:44)
• [isabelle] New AFP entry: Soundness and Completeness of I... (1 message, latest: Sep 19 2022 at 18:11)
• [isabelle] [TFP 2023 Call for Papers] 24th International ... (1 message, latest: Sep 19 2022 at 18:00)
• [isabelle] Isabelle2022-RC0: Export to Scala (3 messages, latest: Sep 19 2022 at 09:22)
• [isabelle] Isabelle2022-RC0: Simp-rules for bit (5 messages, latest: Sep 19 2022 at 09:22)
• [isabelle] Auto-Formatter or Auto-Prettyprinter? (3 messages, latest: Sep 19 2022 at 09:01)
• [isabelle] Code generation in batch mode? (2 messages, latest: Sep 17 2022 at 09:43)
• [isabelle] 2nd CfP - Software Verification and Testing Tr... (1 message, latest: Sep 17 2022 at 07:47)
• [isabelle] [EXTERNAL] Inquiry: Country of Origin for Isab... (1 message, latest: Sep 15 2022 at 13:09)
• [isabelle] Inquiry: Country of Origin for Isabelle Software (3 messages, latest: Sep 15 2022 at 12:07)
• [isabelle] CFP - JFLA 2023 - Journées Francophones des La... (1 message, latest: Sep 14 2022 at 13:30)
• [isabelle] CfP - 29th International Symposium on Model Ch... (1 message, latest: Sep 14 2022 at 09:51)
• [isabelle] New in the AFP: Unbounded Separation Logic (1 message, latest: Sep 14 2022 at 08:34)
• [isabelle] canonical citations for Isabelle/HOL and Sledg... (3 messages, latest: Sep 13 2022 at 21:01)
• [isabelle] Isabelle2022-RC1 available for testing (1 message, latest: Sep 11 2022 at 10:59)
• [isabelle] New in the AFP: Correctness of a Set-Based Alg... (1 message, latest: Sep 09 2022 at 08:09)
• [isabelle] new in the AFP: CRYSTALS-Kyber (1 message, latest: Sep 08 2022 at 15:58)
• [isabelle] New in the AFP: Khovanskii's Theorem (1 message, latest: Sep 07 2022 at 13:39)
• [isabelle] One PhD Position in LogiCS@TUWien Doctoral Pro... (1 message, latest: Sep 07 2022 at 12:47)
• [isabelle] New in the AFP: The Number-Theoretic Transform (1 message, latest: Sep 07 2022 at 11:12)
• [isabelle] New in the AFP: The Hales-Jewett Theorem (1 message, latest: Sep 07 2022 at 09:16)
• [isabelle] “New order prover” (2 messages, latest: Sep 06 2022 at 09:54)
• [isabelle] Call for Papers: Unsound - Sources of Unsoundn... (2 messages, latest: Sep 02 2022 at 20:43)
• [isabelle] Last call for participation: EuroProofNet Work... (3 messages, latest: Sep 01 2022 at 12:11)
• [isabelle] Archive of the Mailing List on Zulip (1 message, latest: Sep 01 2022 at 08:43)
• [isabelle] Positions for Postdocs and Ph.D. candidates (1 message, latest: Sep 01 2022 at 06:57)
• [isabelle] Formal Methods Teaching Workshop (FMTea 2023) ... (1 message, latest: Aug 31 2022 at 17:04)
• [isabelle] CfP Software Verification and Testing Track at... (1 message, latest: Aug 30 2022 at 10:24)
• [isabelle] AFP AxiomaticCategoryTheory and smt_oracle (4 messages, latest: Aug 29 2022 at 10:07)
• [isabelle] Call for Participation: Computational Logic Au... (3 messages, latest: Aug 28 2022 at 13:11)
• [isabelle] global_interpretation of residues fails (3 messages, latest: Aug 25 2022 at 06:15)
• [isabelle] Isabelle2022-RC0: type inference and the unit ... (1 message, latest: Aug 24 2022 at 22:20)
• [isabelle] Inheritance of locales (6 messages, latest: Aug 22 2022 at 21:02)
• [isabelle] new AFP entry: Nano_JSON (1 message, latest: Aug 22 2022 at 18:54)
• [isabelle] CfP: 8th International Workshop on Formal Tec... (1 message, latest: Aug 19 2022 at 20:33)
• [isabelle] Induction generalising the type (1 message, latest: Aug 18 2022 at 12:36)
• [isabelle] Naproche-SAD Error (1 message, latest: Aug 16 2022 at 22:36)
• [isabelle] Certified Programs and Proofs (CPP) 2023 Call ... (2 messages, latest: Aug 16 2022 at 16:07)
• [isabelle] New in the AFP: Simultaneous Diagonalization o... (1 message, latest: Aug 16 2022 at 15:11)
• [isabelle] From the BOOK to the AFP: Two Squares via Invo... (1 message, latest: Aug 15 2022 at 15:39)
• [isabelle] IFL22: Early registration deadline August 15th (1 message, latest: Aug 15 2022 at 09:47)
• [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] 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] 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] 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] 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: Sep 02 2026 at 16:10 UTC