Stream: General

Topics:

• Issues with git integration in vscode (5 messages, latest: Oct 23 2026 at 12:23)
• Document generation fails if \<Zprime> is used in theory (2 messages, latest: Oct 16 2026 at 09:44)
• What triggers rebuild of HOL? (3 messages, latest: Oct 01 2026 at 17:51)
• What is the "native" logic of Isabelle? (5 messages, latest: Sep 25 2026 at 09:34)
• Differences between Simple Type Theory and Isabelle/HOL (2 messages, latest: Sep 15 2026 at 20:09)
• `HOL.Set` and axiomatic set theory (7 messages, latest: Sep 15 2026 at 11:42)
• HOL build fails (7 messages, latest: Sep 08 2026 at 10:17)
• AFP 2025-2 entries failing (4 messages, latest: Aug 31 2026 at 15:21)
• Debugging Isabelle/ML (1 message, latest: Aug 27 2026 at 11:34)
• Usage of AI (9 messages, latest: Aug 24 2026 at 19:14)
• announcement: isabelle-query (2 messages, latest: Aug 21 2026 at 23:20)
• Isabelle website is down (2 messages, latest: Aug 08 2026 at 11:20)
• Books about theory behind proof checking (11 messages, latest: Aug 04 2026 at 23:14)
• [meta] an advice channel for tips/tricks we may stumble upon (18 messages, latest: Aug 04 2026 at 17:44)
• Is `binder_datatype` working in Isabelle2025-2? (4 messages, latest: Jul 31 2026 at 21:40)
• Pre-Workshop Dinner (1 message, latest: Jul 22 2026 at 23:15)
• Concrete-semantics not reachable (2 messages, latest: Jul 20 2026 at 17:35)
• Bruck Ryser Chowla theorem, odd v part (7 messages, latest: Jul 19 2026 at 05:16)
• Conflict of type arities: (1 message, latest: Jul 13 2026 at 12:50)
• Possible leak of CNF files during Sledgehammer invocations (10 messages, latest: Jul 01 2026 at 19:53)
• Importing from HOL (6 messages, latest: Jun 17 2026 at 17:20)
• Reusing session heaps across CI cache restores (4 messages, latest: Jun 11 2026 at 09:39)
• Announcing IsabelleBlueprint (1 message, latest: Jun 01 2026 at 18:23)
• Bug In isabelle linter: appends "theory" to keyword (13 messages, latest: May 04 2026 at 10:07)
• Semantic domain over all recursive function types as output (2 messages, latest: Apr 25 2026 at 09:34)
• Strange definition for `Fun.f_the_inv_into_f_bij_betw` (6 messages, latest: Apr 22 2026 at 14:58)
• Isabelle2025/2025-2 disk permissions on windows (3 messages, latest: Mar 31 2026 at 13:49)
• Isabelle/VSCode server occasionally stops responding (3 messages, latest: Mar 30 2026 at 14:00)
• How to automate relator derivations? (2 messages, latest: Mar 23 2026 at 14:37)
• Derivation of "False" while sledgehammer is working (5 messages, latest: Mar 20 2026 at 21:02)
• Using Isabelle2025-2 vscode on an older codebase (3 messages, latest: Mar 18 2026 at 15:03)
• Looking for proofs of false, Isabelle edition (11 messages, latest: Mar 17 2026 at 12:32)
• Isabelle plugin load error (3 messages, latest: Mar 17 2026 at 10:06)
• Bad theory import FuncSet (4 messages, latest: Mar 15 2026 at 09:08)
• Recursion theorem on some inductive datatype constructors (5 messages, latest: Mar 10 2026 at 14:30)
• Isabelle/jEdit becomes unstable after sledgehammer (11 messages, latest: Mar 08 2026 at 23:51)
• Generative artificial intelligence for mining the AFP (2 messages, latest: Mar 02 2026 at 11:20)
• Can symbols like \<forall> be stored as ∀ instead? (29 messages, latest: Feb 25 2026 at 15:46)
• Apparent redundancies / omissions in HOL-Library.Finite_Map (4 messages, latest: Feb 24 2026 at 20:56)
• Nitpick seems to find invalid counterexample (2 messages, latest: Feb 24 2026 at 16:34)
• parametric typedef based on constant declarations (3 messages, latest: Feb 20 2026 at 09:57)
• Command show ?thesis does not work (11 messages, latest: Feb 13 2026 at 14:52)
• Table.ML slow with very small elements (2 messages, latest: Feb 09 2026 at 12:16)
• AFP down? (3 messages, latest: Feb 01 2026 at 23:52)
• Converse relation notation (3 messages, latest: Jan 30 2026 at 10:38)
• Isabelle's fun package raises an exception (17 messages, latest: Jan 29 2026 at 14:29)
• datatype size (3 messages, latest: Jan 29 2026 at 14:18)
• Finite Cartesian Product of algabraic structures (1 message, latest: Jan 24 2026 at 09:29)
• result may not contain obtained parameters, why? (8 messages, latest: Jan 22 2026 at 09:55)
• Recover green Back and Forward arrows in isabelle jedit (5 messages, latest: Jan 21 2026 at 15:33)
• Isabelle2025-1 in nixpkgs (1 message, latest: Jan 14 2026 at 16:35)
• Procedure for AFP (8 messages, latest: Jan 06 2026 at 23:57)
• FindFacts down? (16 messages, latest: Jan 06 2026 at 11:27)
• Artificial intelligence for Isabelle (28 messages, latest: Dec 29 2025 at 13:52)
• Isabelle on PolyML master (1 message, latest: Dec 26 2025 at 04:41)
• temp Adding a size_definition to the termination solve (1 message, latest: Dec 17 2025 at 11:32)
• Performance gains of having bicompose/biresolution in kernel (8 messages, latest: Dec 04 2025 at 20:03)
• Isabelle 2025-1-RC1 try0 (4 messages, latest: Nov 19 2025 at 12:59)
• Isabelle/VSCode word dictionary and suggestions (3 messages, latest: Nov 19 2025 at 11:13)
• Isabelle 2025-1-RC1 jedit toolbar woes (6 messages, latest: Nov 17 2025 at 16:07)
• UI Scaling (2 messages, latest: Nov 17 2025 at 00:54)
• printing types in non-ML notation (3 messages, latest: Nov 06 2025 at 20:15)
• code_pred not working (1 message, latest: Nov 05 2025 at 01:06)
• Rewrite inside the premise of ⟹ in a custom method (9 messages, latest: Nov 03 2025 at 18:53)
• Loading all theories in a large AFP development (3 messages, latest: Oct 29 2025 at 12:18)
• Making isabelle run on modern z3. (144 messages, latest: Oct 22 2025 at 05:07)
• jEdit font size, Macbook (2 messages, latest: Oct 12 2025 at 00:05)
• What to do if the prover process hangs? (9 messages, latest: Oct 07 2025 at 15:14)
• M4 Macbook Air vs Pro (8 messages, latest: Oct 03 2025 at 07:59)
• description operators in Isabelle/HOL (4 messages, latest: Sep 23 2025 at 17:48)
• Isabelle installation issues (4 messages, latest: Sep 17 2025 at 15:11)
• Circularity and infinite chains in the locale hierarchy (4 messages, latest: Sep 17 2025 at 11:38)
• ITP 2025 plans (5 messages, latest: Sep 08 2025 at 13:07)
• Isabelle for a topic discussed by Einstein (1 message, latest: Sep 04 2025 at 08:54)
• Narrowing the search space (3 messages, latest: Aug 29 2025 at 00:36)
• Functional Datastructures Website hacked? (4 messages, latest: Aug 14 2025 at 08:23)
• What to export from a development? (1 message, latest: Aug 13 2025 at 10:16)
• Repeated integral for ordered indices (2 messages, latest: Aug 04 2025 at 12:47)
• publicly accessible mirror of isabelle (4 messages, latest: Aug 01 2025 at 12:07)
• Naming suggestions for subadditivity? (1 message, latest: Jul 20 2025 at 15:50)
• Cook Levin library (23 messages, latest: Jul 15 2025 at 16:43)
• Module systems (3 messages, latest: Jul 10 2025 at 12:34)
• Bug report (1 message, latest: Jul 06 2025 at 19:10)
• Asking for help (25 messages, latest: Jun 24 2025 at 03:41)
• Is the Isabelle Logo "Open Source"? (6 messages, latest: Jun 18 2025 at 20:52)
• New AFP entry depending on modification of existing entry (4 messages, latest: Jun 10 2025 at 21:21)
• Pretty printing definitions/theorems/abbreviation (1 message, latest: Jun 03 2025 at 15:41)
• Calculational chaining forgets original Left Hand Side (5 messages, latest: Jun 02 2025 at 18:33)
• Naming definitions of a derived locale (5 messages, latest: May 29 2025 at 10:10)
• Building Isabelle_setup (7 messages, latest: May 17 2025 at 05:14)
• Invoking Isabelle/ML from Isabelle/Scala (1 message, latest: May 12 2025 at 09:04)
• Axiom of Choice origin and application in higher order logic (2 messages, latest: May 08 2025 at 10:39)
• Isabelle/Scala component external package support (6 messages, latest: May 05 2025 at 11:31)
• Isabelle2025 in nixpkgs (1 message, latest: May 02 2025 at 15:44)
• Questions about "fix" (63 messages, latest: Apr 15 2025 at 02:06)
• Suppressing document generation when building sessions (1 message, latest: Apr 08 2025 at 15:13)
• simproc for boolean algebra broken? (2 messages, latest: Mar 30 2025 at 12:01)
• Renaming a .thy file gives `bad theory name` (23 messages, latest: Mar 25 2025 at 14:54)
• Profiling, i.e. finding the proof steps, that take long (9 messages, latest: Mar 24 2025 at 21:02)
• Using existing body of formalised mathematical knowledge (3 messages, latest: Mar 24 2025 at 09:08)
• LaTeX documents without proof methods (1 message, latest: Mar 18 2025 at 10:50)
• Developing a theory (1 message, latest: Mar 17 2025 at 09:57)
• Timed out proofs (7 messages, latest: Mar 14 2025 at 16:40)
• Retrieve all registered BNFs (7 messages, latest: Mar 13 2025 at 15:12)
• AFP Fork Date (19 messages, latest: Mar 07 2025 at 17:18)
• more specific way of retrieving code setup? (3 messages, latest: Mar 06 2025 at 09:12)
• Retrieving proof state via Isabelle/Scala (1 message, latest: Mar 06 2025 at 06:30)
• Speeding up isabelle scala build times (1 message, latest: Mar 05 2025 at 15:52)
• How should I define a linear operator in a vector space (5 messages, latest: Feb 26 2025 at 16:28)
• Case expression vs pattern matching in a locale (2 messages, latest: Feb 21 2025 at 11:03)
• vscode not working after 24.04 update (from 23.10 ubuntu) (14 messages, latest: Feb 19 2025 at 16:28)
• Isabelle/VSCode in Isabelle2025-RC0 (7 messages, latest: Feb 18 2025 at 12:09)
• Referring types from constituent locale of a locale addition (6 messages, latest: Feb 10 2025 at 16:31)
• Duplicate fact declaration when interpreting wo_rel (7 messages, latest: Feb 04 2025 at 21:44)
• Starting Isabelle session using Isabelle/Scala (7 messages, latest: Jan 31 2025 at 09:31)
• Bounded lambda abstraction (2 messages, latest: Jan 15 2025 at 14:46)
• Isabelle implementation of locales (1 message, latest: Jan 15 2025 at 10:15)
• How to use Isabelle scalac wrapper in build.sbt (6 messages, latest: Jan 15 2025 at 08:17)
• I've apparently proven a false theorem in Isabelle. (5 messages, latest: Jan 10 2025 at 14:36)
• Generated Scala code doesn't compile because of String (5 messages, latest: Jan 06 2025 at 13:10)
• Getting proof of termination/cong rules for code equations (21 messages, latest: Jan 06 2025 at 09:58)
• Peculiar feature of the proof of the BRC thm part 2 (28 messages, latest: Dec 24 2024 at 01:38)
• Peculiar feature of the proof of the Bruck Ryser Chowla thm (10 messages, latest: Dec 22 2024 at 01:01)
• AFP abstract and metadata (4 messages, latest: Dec 16 2024 at 15:37)
• Embedding Isabelle in another prover - how to reduce size? (22 messages, latest: Dec 11 2024 at 10:00)
• proof using exI (40 messages, latest: Nov 28 2024 at 00:59)
• Primitive constant specification (1 message, latest: Nov 18 2024 at 09:11)
• Storing heap images in custom directory (4 messages, latest: Nov 15 2024 at 01:30)
• Run out of store errors when building sessions (6 messages, latest: Nov 10 2024 at 16:18)
• sledgeham: exception Io {cause = SysErr ("Access is denied." (34 messages, latest: Nov 04 2024 at 00:34)
• isabelle-dev on NixOS (6 messages, latest: Oct 22 2024 at 23:48)
• matrix multiplication (42 messages, latest: Oct 16 2024 at 12:08)
• Proof automation (8 messages, latest: Oct 12 2024 at 17:45)
• Running Isabelle on Linux systems with musl-libc (32 messages, latest: Oct 10 2024 at 00:44)
• Isabelle/ML-Isabelle/Scala Interaction (14 messages, latest: Sep 25 2024 at 10:06)
• Link to Concept in the AFP (6 messages, latest: Sep 24 2024 at 08:11)
• Isabelle/ML function turns state mode to proof mode (10 messages, latest: Sep 23 2024 at 14:37)
• When to cast and when not to cast (6 messages, latest: Sep 23 2024 at 03:12)
• Isabelle crashes: EXCEPTION_ACCESS_VIOLATION (0xc0000005) (13 messages, latest: Sep 16 2024 at 16:21)
• instantiation with same type (7 messages, latest: Sep 16 2024 at 12:29)
• Workaround for duplicate theory name clash? (4 messages, latest: Sep 15 2024 at 10:26)
• Some unicode characters fail to render in jedit (8 messages, latest: Sep 14 2024 at 06:51)
• summation swaps (38 messages, latest: Sep 10 2024 at 12:01)
• vscode_html_output (15 messages, latest: Sep 05 2024 at 08:15)
• frule for elim rules (2 messages, latest: Sep 03 2024 at 14:16)
• Exception Interrupt_Breakdown: why and how to solve? (12 messages, latest: Sep 03 2024 at 10:49)
• Super_sketch tool: generating multiple sledgehammer proofs (2 messages, latest: Sep 02 2024 at 13:20)
• Most reproved theorems (14 messages, latest: Aug 23 2024 at 07:37)
• Feeding searched lemmas to Sledgehammer (2 messages, latest: Aug 22 2024 at 09:37)
• What happened to isabelle.systems? (4 messages, latest: Aug 22 2024 at 07:26)
• incorrect counterexamples? (24 messages, latest: Aug 22 2024 at 05:36)
• Illegal dummy pattern (3 messages, latest: Aug 14 2024 at 12:40)
• Computer recommendations (11 messages, latest: Aug 14 2024 at 10:49)
• global theories (3 messages, latest: Aug 12 2024 at 08:06)
• How to use is_square (16 messages, latest: Jul 31 2024 at 02:47)
• AFP entry submission from link not working (1 message, latest: Jul 29 2024 at 08:20)
• Building Isabelle from scratch (14 messages, latest: Jul 26 2024 at 21:14)
• Problems with square roots (39 messages, latest: Jul 25 2024 at 09:41)
• Determinant properties of incidence matrix (18 messages, latest: Jul 16 2024 at 18:09)
• [fundef_cong] causes exception CYCLES (8 messages, latest: Jul 15 2024 at 08:40)
• Existentially quantified type (1 message, latest: Jul 13 2024 at 12:49)
• Isabelle2024 in nixpkgs (1 message, latest: Jul 07 2024 at 13:08)
• Consumer thread failure: "Isabelle.command_input" (1 message, latest: Jul 02 2024 at 17:48)
• "not of sort enum" error with code generation (9 messages, latest: Jun 06 2024 at 09:40)
• Transforming a proof state from "state" mode to "prove" mode (4 messages, latest: Jun 05 2024 at 10:43)
• Defining awkward binder syntax (5 messages, latest: May 31 2024 at 08:12)
• Ignore specific premises in `simp` (3 messages, latest: May 26 2024 at 19:41)
• Course Material (update, fix broken links) (2 messages, latest: May 18 2024 at 07:04)
• sledgehammer_commands.ML: how to use (13 messages, latest: May 16 2024 at 22:08)
• Polymorphic typedef with typeclass restriction (2 messages, latest: May 16 2024 at 15:35)
• batch mode quick_and_dirty, but longer timeout for provers (1 message, latest: May 16 2024 at 09:49)
• running Isabelle in batch mode: how to use? (4 messages, latest: May 15 2024 at 09:46)
• Redirecting sledgehammer output to file instead (28 messages, latest: May 10 2024 at 04:54)
• Lemmas about mod division qualified in RC2024 (5 messages, latest: May 07 2024 at 09:13)
• Time Out connecting AFP (4 messages, latest: May 06 2024 at 17:36)
• Foldable output (2 messages, latest: May 06 2024 at 05:09)
• Switching Isabelle version for command line tools (4 messages, latest: May 05 2024 at 08:32)
• tools to automatically adopt sledgehammer proofs into theory (9 messages, latest: May 03 2024 at 14:55)
• Trimming proof state output (20 messages, latest: May 03 2024 at 05:18)
• Identifying & deleting claset rule (7 messages, latest: May 02 2024 at 09:25)
• Adding to Talia Ringer's list of resources? (2 messages, latest: Apr 23 2024 at 04:02)
• Conversion between expanded and compact form of same lemma (1 message, latest: Apr 22 2024 at 13:48)
• Devel website is suddenly out of date (6 messages, latest: Apr 15 2024 at 15:15)
• Beyond Freek Wiedijk's 100 theorem (10 messages, latest: Mar 29 2024 at 10:57)
• Type unification problem (4 messages, latest: Mar 19 2024 at 16:54)
• Getting Jedit to render math symbols consistently (2 messages, latest: Mar 16 2024 at 07:06)
• Printing out all subgoals when there are many (7 messages, latest: Mar 14 2024 at 13:42)
• Dubious type error (6 messages, latest: Mar 13 2024 at 15:55)
• Metis: The assumptions are inconsistent (9 messages, latest: Mar 13 2024 at 13:56)
• dark mode in isabelle output (2 messages, latest: Mar 12 2024 at 02:20)
• Enter Match Example (4 messages, latest: Feb 27 2024 at 13:14)
• (How) can I declare a domain a codatatype (or vice-versa)? (3 messages, latest: Feb 26 2024 at 14:50)
• Ubuntu Snapcraft package (1 message, latest: Feb 25 2024 at 02:22)
• Where to find the AFP for Isabelle2021 onwards? (3 messages, latest: Feb 19 2024 at 09:08)
• What is your CPU - do you use AMD? (5 messages, latest: Feb 19 2024 at 05:52)
• nunchaku: unsupported lower-level constant Rep_ (1 message, latest: Feb 16 2024 at 14:46)
• Locales "extra type variables in a type constant instance" (1 message, latest: Feb 15 2024 at 12:54)
• Stating that a structure conforms a locale (1 message, latest: Feb 15 2024 at 11:30)
• Isabelle development version (3 messages, latest: Feb 09 2024 at 13:25)
• Finding an old library theorem (5 messages, latest: Feb 09 2024 at 11:18)
• Methods erule and drule in Isar proofs (4 messages, latest: Feb 09 2024 at 11:15)
• Right side window in Isabelle/jEdit (2 messages, latest: Jan 24 2024 at 12:42)
• Tools build on top (3 messages, latest: Jan 13 2024 at 07:55)
• Cambridge seminar series resuming! (1 message, latest: Jan 12 2024 at 13:37)
• Bug reports (4 messages, latest: Jan 07 2024 at 19:20)
• Isabelle not using introduced notation in sublocale (2 messages, latest: Dec 26 2023 at 00:02)
• Isabelle2023 in nixpkgs (1 message, latest: Dec 13 2023 at 11:30)
• Problem with \endisadelimproof in typesetting (4 messages, latest: Dec 06 2023 at 14:39)
• How can I import AutoCorres? (3 messages, latest: Dec 04 2023 at 10:59)
• No unicode symbols (8 messages, latest: Nov 29 2023 at 17:44)
• Building a heap image for a built-in theory (8 messages, latest: Nov 22 2023 at 12:58)
• Single rule expected in cases proof (4 messages, latest: Nov 17 2023 at 15:25)
• isabelle server is slow (1 message, latest: Nov 02 2023 at 08:59)
• verbatim lemma can't prove subgoal (9 messages, latest: Nov 01 2023 at 11:31)
• Mizar-style single step reasoning in Isabelle proofs (5 messages, latest: Oct 25 2023 at 21:50)
• Auto expansion in Isabelle/jEdit (1 message, latest: Oct 20 2023 at 12:49)
• Vampire: problem is unprovable (13 messages, latest: Oct 17 2023 at 13:52)
• Let simplification (5 messages, latest: Oct 12 2023 at 11:46)
• Stylistic advice for logic involving partial functions (8 messages, latest: Oct 09 2023 at 09:09)
• Meta-forall order (4 messages, latest: Oct 02 2023 at 13:41)
• CryptHOL: proof obvious advantage difference (8 messages, latest: Sep 30 2023 at 13:46)
• Providing cases, induct and coinduct rules (2 messages, latest: Sep 28 2023 at 16:41)
• Functions defined with keyword function (8 messages, latest: Sep 28 2023 at 15:58)
• Surprising definitions of True and False. (10 messages, latest: Sep 25 2023 at 08:46)
• Detecting Vacuously True Propositions (6 messages, latest: Sep 24 2023 at 21:35)
• Derived False (1 message, latest: Sep 22 2023 at 09:02)
• Attributes and locale interpretations (1 message, latest: Sep 21 2023 at 13:40)
• Case distinction on returned constructor (6 messages, latest: Sep 20 2023 at 15:07)
• A surprising failure to unify (4 messages, latest: Sep 20 2023 at 05:01)
• Strategy for proving FSet theorems (5 messages, latest: Sep 19 2023 at 20:31)
• Why can't we take the domain of an arbitrary function? (6 messages, latest: Sep 18 2023 at 10:19)
• Finite set type? (6 messages, latest: Sep 14 2023 at 17:18)
• Naming the lemmas of a theory (3 messages, latest: Sep 14 2023 at 15:10)
• Groups_Big type problem (5 messages, latest: Sep 14 2023 at 12:59)
• Ctrl-click in finished theories (5 messages, latest: Sep 13 2023 at 17:08)
• Continuous ML Cleanup (6 messages, latest: Sep 13 2023 at 11:08)
• Calling Isabelle incrementally on command line (10 messages, latest: Sep 08 2023 at 11:36)
• factorial_monoid interpretation (2 messages, latest: Sep 06 2023 at 13:00)
• conditinoal comprehension rewriting (14 messages, latest: Aug 31 2023 at 21:05)
• Rust (7 messages, latest: Aug 31 2023 at 20:19)
• Reverse matching with Eisbach not working? (2 messages, latest: Aug 22 2023 at 20:36)
• What’s the difference between `rewrite at` and `rewrite in`? (3 messages, latest: Aug 15 2023 at 20:41)
• Splitting with nested patterns (14 messages, latest: Aug 14 2023 at 20:48)
• Syntax transformation that introduces variable binding (8 messages, latest: Aug 12 2023 at 12:49)
• Polymorphic corecursive definition not accepted (14 messages, latest: Aug 08 2023 at 05:32)
• How to disable dictionary suggestions in Isabelle/VSCode (1 message, latest: Aug 07 2023 at 12:59)
• Proof checking on remote server (17 messages, latest: Aug 03 2023 at 05:51)
• Head of empty list (9 messages, latest: Aug 02 2023 at 19:29)
• Amending an interpretation (6 messages, latest: Aug 02 2023 at 13:54)
• EuroProofNet Workshops, Cambridge, UK, Sept. 6-8 2023 (2 messages, latest: Jul 19 2023 at 17:38)
• Prettyprinting function on a finite domain (6 messages, latest: Jul 18 2023 at 13:33)
• using value command result for proofs (11 messages, latest: Jul 10 2023 at 10:43)
• Isabelle Ultras (29 messages, latest: Jul 03 2023 at 11:15)
• Solver z3 terminated abnormally (2 messages, latest: Jun 28 2023 at 14:34)
• Efficient session loading from AFP (24 messages, latest: Jun 24 2023 at 11:04)
• Citing AFP (6 messages, latest: Jun 23 2023 at 10:07)
• Syntax highlighting (6 messages, latest: Jun 20 2023 at 12:35)
• Type construction (1 message, latest: Jun 15 2023 at 15:14)
• Proving set membership in a type (6 messages, latest: Jun 14 2023 at 18:45)
• codegen for predicates (19 messages, latest: Jun 06 2023 at 17:01)
• Isabelle/VSCode Github Copilot (6 messages, latest: Jun 02 2023 at 08:44)
• How does `adhoc_overloading` work? (6 messages, latest: May 15 2023 at 13:07)
• Datatype record update (3 messages, latest: Apr 20 2023 at 08:59)
• Compiling jEdit (1 message, latest: Apr 11 2023 at 08:20)
• Error loading webview (3 messages, latest: Apr 10 2023 at 13:41)
• Refactoring syntax (3 messages, latest: Apr 06 2023 at 16:37)
• Where is the `coinduction` proof method documented? (2 messages, latest: Mar 31 2023 at 20:20)
• UNIV in Isabelle Probability (2 messages, latest: Mar 29 2023 at 09:57)
• Antiquotation for locale or syntax to be defined (3 messages, latest: Mar 22 2023 at 12:43)
• No auto_nitpick (4 messages, latest: Mar 14 2023 at 15:40)
• Visual Studio Code extension (2 messages, latest: Mar 13 2023 at 17:16)
• Github Workflows for Isabelle (6 messages, latest: Mar 07 2023 at 10:42)
• problems with leamma proving (1 message, latest: Mar 02 2023 at 11:07)
• How can I limit the memory usage of Poly/ML? (4 messages, latest: Feb 23 2023 at 06:11)
• How to build from source? (3 messages, latest: Feb 16 2023 at 04:48)
• Function between two locale (7 messages, latest: Feb 04 2023 at 16:46)
• Proofs with orderings on Words (3 messages, latest: Jan 29 2023 at 02:52)
• Sepref implemntation Binding (2 messages, latest: Jan 27 2023 at 15:32)
• DOI For AFP Entries (14 messages, latest: Jan 27 2023 at 11:27)
• Multi-sort atoms in Nominal2 (3 messages, latest: Jan 23 2023 at 17:06)
• Definition of topological filters (4 messages, latest: Jan 15 2023 at 12:02)
• Code Generation "Show" overrides (1 message, latest: Jan 13 2023 at 18:52)
• Entering special symbols in Isabelle/VSCode (16 messages, latest: Jan 13 2023 at 18:28)
• Forcing a redraw of a Isabelle/VSCode file view (4 messages, latest: Jan 11 2023 at 02:29)
• Sum of nats = int (Sum of (2 messages, latest: Jan 09 2023 at 21:13)
• Schematics in Eisbach (1 message, latest: Dec 29 2022 at 09:06)
• ✔ Isabelle making my computer hang (1 message, latest: Dec 11 2022 at 18:17)
• Isabelle2022 in nixpkgs (2 messages, latest: Dec 10 2022 at 11:00)
• Isabelle making my computer hang (7 messages, latest: Dec 10 2022 at 10:58)
• Instantiate schematic variables in goal (4 messages, latest: Dec 08 2022 at 16:11)
• ✔ AFP entry broken (3 messages, latest: Dec 01 2022 at 23:03)
• AFP entry broken (3 messages, latest: Dec 01 2022 at 21:16)
• isabelle-emacs package (23 messages, latest: Dec 01 2022 at 08:19)
• ✔ Map type, hashmap with sepref (1 message, latest: Nov 30 2022 at 21:22)
• Map type, hashmap with sepref (15 messages, latest: Nov 30 2022 at 14:48)
• ✔ More Debug Info in Batch Build (2 messages, latest: Nov 24 2022 at 13:26)
• More Debug Info in Batch Build (2 messages, latest: Nov 24 2022 at 09:46)
• autoformalisation (1 message, latest: Nov 22 2022 at 14:15)
• ✔ Imperative code generation (1 message, latest: Nov 17 2022 at 10:09)
• Imperative code generation (5 messages, latest: Nov 15 2022 at 12:19)
• Tutorials are missing (4 messages, latest: Nov 14 2022 at 12:53)
• simp looping on trivial goal (20 messages, latest: Nov 08 2022 at 08:56)
• schematic goals with Eps (15 messages, latest: Nov 06 2022 at 16:40)
• Job announcements (2 messages, latest: Oct 14 2022 at 11:39)
• ✔ Export code from command line (1 message, latest: Oct 07 2022 at 13:01)
• ✔ Missing lemma in `List` (2 messages, latest: Oct 05 2022 at 14:35)
• Missing lemma in `List` (6 messages, latest: Oct 05 2022 at 14:16)
• String export (1 message, latest: Oct 05 2022 at 14:00)
• Isabelle omega, a good idea? (3 messages, latest: Sep 20 2022 at 11:32)
• Isabelle2022-RC2 for nixos (1 message, latest: Sep 19 2022 at 20:46)
• Export code from command line (6 messages, latest: Sep 13 2022 at 08:27)
• frequent GC when memory is sufficient (3 messages, latest: Aug 27 2022 at 14:25)
• How might I go about creating a code generation target? (10 messages, latest: Jul 20 2022 at 20:36)
• Liquid tensor experiment (9 messages, latest: Jul 16 2022 at 07:34)
• Problems with \<^bsub>...\<^esub> (10 messages, latest: Jun 14 2022 at 15:41)
• New paper on machine learning for Isabelle (1 message, latest: May 26 2022 at 10:01)
• Generalizing exp limit (6 messages, latest: May 23 2022 at 14:32)
• Persistent assumption attributes (1 message, latest: May 09 2022 at 10:04)
• stream events (1 message, latest: May 06 2022 at 07:15)
• ✔ Type constructor variables (5 messages, latest: Apr 15 2022 at 13:50)
• Seeking Isabelle ConNF formalisation (3 messages, latest: Apr 07 2022 at 13:30)
• isabelle-linter in nixpkgs (2 messages, latest: Mar 29 2022 at 14:42)
• Classes (1 message, latest: Mar 18 2022 at 20:05)
• ✔ Partial termination proofs (12 messages, latest: Mar 18 2022 at 18:04)
• Top level term rewriting (1 message, latest: Mar 12 2022 at 14:14)
• ✔ Induction rule for Jinja.Kildall (3 messages, latest: Mar 11 2022 at 22:50)
• ✔ resolve_tac but only doing unification (7 messages, latest: Mar 10 2022 at 14:31)
• Shortcut to complete "active markup" (2 messages, latest: Mar 03 2022 at 13:59)
• ✔ `quick_and_dirty` mode skips regular proofs (3 messages, latest: Feb 21 2022 at 14:07)
• Workshop: Machine-Checked Mathematics (4 messages, latest: Feb 20 2022 at 13:04)
• ✔ enumerating non-constructor patterns (6 messages, latest: Feb 09 2022 at 19:34)
• ROOT help (5 messages, latest: Feb 04 2022 at 17:41)
• ✔ `\<comment>` after `text` omitted in LaTeX output (3 messages, latest: Feb 03 2022 at 18:14)
• Divergence thm and Cauchy-Goursat (9 messages, latest: Feb 02 2022 at 11:08)
• Isabelle2021 nixpkgs (6 messages, latest: Jan 30 2022 at 14:07)
• translations with ambiguous types (9 messages, latest: Jan 19 2022 at 16:36)
• Intuitionistic proof search (1 message, latest: Jan 14 2022 at 19:12)
• Assumption about finite set cardinality not being considered (4 messages, latest: Jan 02 2022 at 20:17)
• ✔ Eta expand for unfolding (4 messages, latest: Jan 02 2022 at 19:58)
• Splitting cases in Universally quantified goals (3 messages, latest: Dec 31 2021 at 14:27)
• Replace higher-order premise (4 messages, latest: Dec 30 2021 at 17:11)
• Destruction of premises with universal quantification (1 message, latest: Dec 30 2021 at 13:58)
• Date functionality (1 message, latest: Dec 12 2021 at 02:00)
• StackExchange proposed site ProofAssistants (1 message, latest: Dec 09 2021 at 12:47)
• ✔ Fixed type variable (4 messages, latest: Dec 08 2021 at 16:14)
• Semantic subytpes + lifting vs. simple predicates (1 message, latest: Dec 08 2021 at 14:40)
• Eisbach matching meta forall in conclusions (11 messages, latest: Dec 07 2021 at 15:10)
• ✔ ML cleanup problems (46 messages, latest: Dec 03 2021 at 12:43)
• ✔ Logarithms (13 messages, latest: Nov 30 2021 at 16:10)
• ✔ Subtypes of ℝ (15 messages, latest: Nov 28 2021 at 21:05)
• ✔ Limit superior (25 messages, latest: Nov 28 2021 at 21:05)
• Exploring Variant of the 'guess' command (13 messages, latest: Nov 25 2021 at 22:21)
• Don’t `?` and `|` perform backtracking? (1 message, latest: Nov 23 2021 at 20:54)
• Translate terminal proof to single method (8 messages, latest: Nov 23 2021 at 15:33)
• ✔ Changes in match variables not considered when backtrac... (5 messages, latest: Nov 21 2021 at 16:30)
• ✔ Broken fact computation in connection with Eisbach (4 messages, latest: Nov 21 2021 at 16:30)
• Zulip Case Study for Formalisation Projects (Lean) (1 message, latest: Nov 19 2021 at 12:54)
• Preventing backtracking (1 message, latest: Nov 08 2021 at 12:57)
• blast fails with no output (5 messages, latest: Nov 08 2021 at 08:51)
• ✔ Isabelle Docker image on GitHub Actions (5 messages, latest: Sep 28 2021 at 16:57)
• String syntax (2 messages, latest: Sep 21 2021 at 16:47)
• Exception while using the lifting package (3 messages, latest: Sep 18 2021 at 19:55)
• ✔ nested subtype, relator (3 messages, latest: Sep 18 2021 at 17:36)
• No relator created for data type involving `set` (3 messages, latest: Sep 11 2021 at 07:15)
• nlinarith for Isabelle (6 messages, latest: Jul 30 2021 at 10:05)
• Does Google index the zulip archive properly? (3 messages, latest: Jul 21 2021 at 21:51)
• Inner syntax antiquotations (3 messages, latest: Jul 16 2021 at 09:22)
• missing isabelle component (10 messages, latest: Jul 05 2021 at 14:22)
• No PDF output (14 messages, latest: Jun 28 2021 at 16:35)
• Defining Eisbach methods with variable length arguments (10 messages, latest: Jun 27 2021 at 16:57)
• Proof Ground 2021 (2 messages, latest: Jun 18 2021 at 13:19)
• Dropping global mixfix syntax (2 messages, latest: May 30 2021 at 12:26)
• AFP submission processing time (3 messages, latest: May 24 2021 at 15:39)
• Optimal Sorting Networks in Isabelle (1 message, latest: May 04 2021 at 14:53)
• Undo hide_fact (open) (1 message, latest: Apr 29 2021 at 09:50)
• delta (8 messages, latest: Apr 27 2021 at 10:52)
• turn subgoal into Isar style statement (27 messages, latest: Apr 20 2021 at 17:18)
• new streams (10 messages, latest: Apr 19 2021 at 11:25)
• jEdit Plugin for Isabelle Symbol suggestions (1 message, latest: Apr 18 2021 at 13:01)
• Programmatic access to Isabelle theories (12 messages, latest: Apr 17 2021 at 19:48)
• Raspberry Pi OS (12 messages, latest: Apr 17 2021 at 16:33)
• Analysis (7 messages, latest: Apr 14 2021 at 13:19)
• "Real" imperative code generation from Isabelle (19 messages, latest: Apr 12 2021 at 13:24)
• IRC (2 messages, latest: Mar 17 2021 at 17:47)
• Isabelle/HOL's proof-theoretic strength (4 messages, latest: Mar 13 2021 at 16:49)
• Isabelle2021 instability (23 messages, latest: Mar 09 2021 at 09:30)
• Download Isabelle2020 (7 messages, latest: Mar 01 2021 at 12:46)
• Random idea: multiway if? (4 messages, latest: Feb 10 2021 at 14:32)
• dependent types and Isar (8 messages, latest: Feb 08 2021 at 13:14)
• isabelle build: ignore timeout (7 messages, latest: Nov 25 2020 at 15:33)
• Application in the presence of schematic types (1 message, latest: Nov 23 2020 at 18:28)
• Debugging output in a tactic (5 messages, latest: Nov 11 2020 at 17:06)
• Change ISABELLE_HOME_USER (3 messages, latest: Nov 11 2020 at 11:29)
• split all case expressions (7 messages, latest: Nov 02 2020 at 17:50)
• Discharging OFCLASS assumption (3 messages, latest: Oct 22 2020 at 13:16)
• proofterm.ML (1 message, latest: Oct 22 2020 at 08:42)
• Undergraduate mathematics in Isabelle (17 messages, latest: Oct 14 2020 at 08:49)
• Continuous integration (61 messages, latest: Sep 21 2020 at 04:48)
• Visual Studio Code Remote + Isabelle (6 messages, latest: Aug 16 2020 at 12:08)
• Generalising to subset (19 messages, latest: Aug 13 2020 at 12:09)
• The context record (1 message, latest: Aug 12 2020 at 11:41)
• Hiding type class instances (31 messages, latest: Aug 11 2020 at 16:42)
• Simplifier.prems_of (24 messages, latest: Aug 06 2020 at 16:44)
• Construct term while instantiating schematic type variables (15 messages, latest: Aug 04 2020 at 15:50)
• Theory namespaces (3 messages, latest: Jul 31 2020 at 11:42)
• Obtaining properly localised terms (1 message, latest: Jul 28 2020 at 09:41)
• Thm.assume: undeclared hyps (10 messages, latest: Jul 23 2020 at 09:23)
• Automatically contracted abbreviations (11 messages, latest: Jul 17 2020 at 15:12)
• Making proofs with inductive predicates easier (7 messages, latest: Jul 17 2020 at 09:16)
• Kolmogorov–Arnol'd superposition theorem (1 message, latest: Jul 15 2020 at 16:07)
• intro vs simp for equality facts (12 messages, latest: Jul 15 2020 at 14:12)
• bundled syntax / translations (1 message, latest: Jul 13 2020 at 15:54)
• Proposal: Functional dependencies for overloaded constants (16 messages, latest: Jun 19 2020 at 11:44)
• Proof Ground 2020 (4 messages, latest: Jun 18 2020 at 07:01)
• fast_term_ord (1 message, latest: Jun 17 2020 at 14:35)
• Simplifier - term ordering (4 messages, latest: Jun 17 2020 at 10:01)
• Reusing heap images (2 messages, latest: May 28 2020 at 11:58)
• Generalized Pigeonhole Principle (8 messages, latest: May 14 2020 at 10:08)
• Cookbook (4 messages, latest: Apr 29 2020 at 16:35)
• Simplify only the assumptions, not the goal (3 messages, latest: Apr 22 2020 at 09:22)
• Schematic variables in goal after intro (12 messages, latest: Apr 07 2020 at 09:52)
• Keep case names with lemmas (3 messages, latest: Mar 30 2020 at 15:26)
• Websites with Isabelle information (6 messages, latest: Mar 29 2020 at 11:54)
• `rewrite` method tutorial (4 messages, latest: Mar 24 2020 at 18:42)
• Hiding flex-flex constraints (10 messages, latest: Mar 24 2020 at 11:34)
• Function "on" (4 messages, latest: Mar 23 2020 at 15:29)
• applying rules/facts up to unification (5 messages, latest: Mar 23 2020 at 13:52)
• Symbol for equivalence (17 messages, latest: Mar 18 2020 at 11:51)
• Convert case rules into split rules (9 messages, latest: Mar 17 2020 at 19:42)
• isabelle build (1 message, latest: Jan 17 2020 at 11:07)
• Editing Pure (3 messages, latest: Dec 06 2019 at 08:27)
• macros for comments (1 message, latest: Nov 14 2019 at 15:56)
• partial derivative (4 messages, latest: Nov 11 2019 at 16:39)
• Automatic indentation (1 message, latest: Nov 11 2019 at 11:02)
• Isabelle code in LaTeX documents (14 messages, latest: Oct 19 2019 at 01:07)
• jEdit (10 messages, latest: Oct 09 2019 at 15:14)
• Applying method n times (6 messages, latest: Oct 01 2019 at 09:05)
• Isabelle Phabricator (1 message, latest: Sep 27 2019 at 08:26)
• show theorems with certain attributes (3 messages, latest: Sep 26 2019 at 12:26)
• Zulip archive (6 messages, latest: Sep 23 2019 at 23:07)
• VS Code (73 messages, latest: Sep 22 2019 at 19:44)
• installation (9 messages, latest: Sep 20 2019 at 15:27)
• unification in induction tactic (2 messages, latest: Sep 18 2019 at 07:07)
• Proving for Fun (7 messages, latest: Sep 13 2019 at 21:18)
• smooth manifold (3 messages, latest: Sep 09 2019 at 17:28)
• Isabelle + Latex (5 messages, latest: Sep 02 2019 at 10:20)
• Online Isabelle (1 message, latest: Aug 30 2019 at 10:12)
• Isabelle on NixOS (3 messages, latest: Aug 30 2019 at 09:08)
• folds (2 messages, latest: Aug 22 2019 at 12:22)
• OptionalSugar (7 messages, latest: Aug 12 2019 at 13:12)
• Programmatically eta-reduce theorem conclusion (3 messages, latest: Aug 11 2019 at 15:28)
• locale (11 messages, latest: Aug 02 2019 at 14:51)
• Isar (3 messages, latest: Jul 31 2019 at 13:10)
• sledgehammer (1 message, latest: Jul 26 2019 at 21:47)
• eisbach (1 message, latest: Jul 17 2019 at 22:45)
• AFP submission guidelines (1 message, latest: Jul 17 2019 at 10:40)
• style guide (1 message, latest: Jul 17 2019 at 10:34)
• smt error (5 messages, latest: Jul 17 2019 at 10:30)
• Streams (4 messages, latest: Jul 14 2019 at 11:46)
• gold standard (2 messages, latest: Jul 06 2019 at 13:43)
• Proofs refactoring (1 message, latest: Jul 06 2019 at 11:45)
• documentation (2 messages, latest: Jul 05 2019 at 09:45)
• GitHub (1 message, latest: Jul 04 2019 at 08:36)
• swimming turtles (1 message, latest: Jul 02 2019 at 12:26)
• topic demonstration (2 messages, latest: Jul 02 2019 at 12:26)

Last updated: Oct 25 2026 at 22:21 UTC