Zulip Chat Archive

Stream: General

Topics:

Command show ?thesis does not work (8 messages, latest: Feb 05 2026 at 22:05)
Nitpick seems to find invalid counterexample (1 message, latest: Feb 02 2026 at 10:06)
AFP down? (3 messages, latest: Feb 01 2026 at 23:52)
Isabelle/jEdit becomes unstable after sledgehammer (2 messages, latest: Jan 31 2026 at 08:09)
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)
Can symbols like \<forall> be stored as ∀ instead? (22 messages, latest: Jan 22 2026 at 09:50)
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)
`HOL.Set` and axiomatic set theory (3 messages, latest: Jun 07 2024 at 13:52)
"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: Feb 06 2026 at 20:37 UTC