Stream: General

Topics:

• Problems with \<^bsub>...\<^esub> (10 messages, latest: Jun 14 2022 at 15:41)
• How might I go about creating a code generation target? (8 messages, latest: May 31 2022 at 17:54)
• 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 (1 message, latest: Mar 18 2022 at 18:04)
• Partial termination proofs (11 messages, latest: Mar 18 2022 at 13:25)
• Top level term rewriting (1 message, latest: Mar 12 2022 at 14:14)
• ✔ Induction rule for Jinja.Kildall (1 message, latest: Mar 11 2022 at 22:50)
• ✔ resolve_tac but only doing unification (6 messages, latest: Mar 10 2022 at 14:31)
• resolve_tac but only doing unification (1 message, latest: Mar 10 2022 at 13:23)
• Shortcut to complete "active markup" (2 messages, latest: Mar 03 2022 at 13:59)
• Induction rule for Jinja.Kildall (2 messages, latest: Feb 25 2022 at 15:25)
• ✔ `quick_and_dirty` mode skips regular proofs (2 messages, latest: Feb 21 2022 at 14:07)
• Workshop: Machine-Checked Mathematics (4 messages, latest: Feb 20 2022 at 13:04)
• `quick_and_dirty` mode skips regular proofs (1 message, latest: Feb 17 2022 at 12:33)
• ✔ 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 (3 messages, latest: Jan 02 2022 at 19:58)
• Eta expand for unfolding (1 message, latest: Jan 02 2022 at 19:12)
• 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 (2 messages, 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 (1 message, latest: Dec 03 2021 at 12:43)
• ✔ Logarithms (12 messages, latest: Nov 30 2021 at 16:10)
• ML cleanup problems (45 messages, latest: Nov 29 2021 at 16:45)
• Logarithms (1 message, latest: Nov 28 2021 at 21:08)
• ✔ Subtypes of ℝ (1 message, latest: Nov 28 2021 at 21:05)
• ✔ Limit superior (21 messages, latest: Nov 28 2021 at 21:05)
• Limit superior (4 messages, latest: Nov 28 2021 at 20:19)
• (no topic) (1 message, latest: Nov 25 2021 at 22:21)
• Exploring Variant of the 'guess' command (12 messages, latest: Nov 25 2021 at 18:35)
• Subtypes of ℝ (14 messages, latest: Nov 25 2021 at 12:28)
• 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... (3 messages, latest: Nov 21 2021 at 16:30)
• ✔ Broken fact computation in connection with Eisbach (1 message, latest: Nov 21 2021 at 16:30)
• Broken fact computation in connection with Eisbach (3 messages, latest: Nov 21 2021 at 16:29)
• Zulip Case Study for Formalisation Projects (Lean) (1 message, latest: Nov 19 2021 at 12:54)
• Changes in match variables not considered when backtracking (2 messages, latest: Nov 11 2021 at 11:10)
• 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 (4 messages, latest: Sep 28 2021 at 16:57)
• String syntax (2 messages, latest: Sep 21 2021 at 16:47)
• Isabelle Docker image on GitHub Actions (1 message, latest: Sep 21 2021 at 12:07)
• Exception while using the lifting package (3 messages, latest: Sep 18 2021 at 19:55)
• ✔ nested subtype, relator (2 messages, latest: Sep 18 2021 at 17:36)
• nested subtype, relator (1 message, latest: Sep 16 2021 at 11:11)
• 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)
• Liquid tensor experiment (5 messages, latest: Jan 06 2021 at 14:28)
• 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: Jul 07 2022 at 02:12 UTC