Stream: General

Topics:

• 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)
• Detecting Vacuously True Propositions (5 messages, latest: Sep 09 2023 at 12:56)
• 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)
• CryptHOL: proof obvious advantage difference (5 messages, latest: Jul 25 2023 at 18:23)
• 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: Sep 22 2023 at 08:19 UTC