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