Topics:
- [meta] an advice channel for tips/tricks we may stumble upon (8 messages, latest: Apr 03 2026 at 20:22)
- `HOL.Set` and axiomatic set theory (4 messages, latest: Apr 01 2026 at 08:48)
- 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)
- What is the "native" logic of Isabelle? (3 messages, latest: Dec 26 2025 at 07:48)
- 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)
- Bruck Ryser Chowla theorem, odd v part (6 messages, latest: Jul 26 2024 at 09:53)
- 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: Apr 09 2026 at 09:11 UTC