Zulip Chat Archive

Stream: General

Topics:

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 19 2024 at 08:19 UTC