Topics:
- Sorts in proof export (4 messages, latest: Aug 14 2026 at 23:29)
- go to definition doesn't always work in Isabelle/ML (11 messages, latest: May 26 2026 at 10:20)
- simproc is not invoked in local theory during a proof in ML (1 message, latest: May 08 2026 at 18:50)
- Sail RISC-C Isabelle build (3 messages, latest: Apr 17 2026 at 19:42)
- Printing terms with type annotations on constants (18 messages, latest: Jan 30 2026 at 12:09)
- Entry point for Sledgehammer’s external prover interface (13 messages, latest: Dec 09 2025 at 06:14)
- Using ML to Automatically Dualize (6 messages, latest: Nov 25 2025 at 07:48)
- Relaxing sort constraints for typedef axioms (1 message, latest: Oct 12 2025 at 20:30)
- Parsing command tokens like "apply" in outer syntax (8 messages, latest: Sep 26 2025 at 00:30)
- Rewrites for object-level equality (18 messages, latest: Sep 16 2025 at 16:09)
- Embedded DSL: Parsing Identifiers Directly Into Strings (2 messages, latest: Aug 16 2025 at 02:00)
- searching for a tactic (8 messages, latest: Jul 28 2025 at 16:46)
- Source-code definition of const (1 message, latest: Apr 02 2025 at 17:22)
- Can you capture the simp trace from Isabelle/ML ? (4 messages, latest: Feb 21 2025 at 18:30)
- safely doing a evaluation of ml evaluation (3 messages, latest: Nov 30 2024 at 09:53)
- Specification.definition vs Local_Theory.define (1 message, latest: Sep 23 2024 at 11:46)
- Parsing lemma in Isar assumes/shows syntax (3 messages, latest: Sep 02 2024 at 18:26)
- Syntax error using pure implication (29 messages, latest: Aug 30 2024 at 09:39)
- Profiling isabelle (2 messages, latest: Aug 22 2024 at 07:31)
- What is the meaning of variables in isabelle? (27 messages, latest: Aug 21 2024 at 08:00)
- metis_tac proving wrong theorem (3 messages, latest: Aug 20 2024 at 08:20)
- Instantiation get instantiated type (2 messages, latest: Aug 13 2024 at 09:32)
- Function Interface (4 messages, latest: Aug 09 2024 at 15:24)
- Lexicons for Scanning (4 messages, latest: Jun 03 2024 at 14:41)
- Parser for Isabelle/ML (10 messages, latest: May 28 2024 at 05:48)
- Remove markup from error strings (4 messages, latest: May 24 2024 at 11:57)
- Extracting goal/proof obligation directly from context (6 messages, latest: May 03 2024 at 08:21)
- Convert a proof method into a tactic? (5 messages, latest: May 02 2024 at 08:58)
- Undo quick_and_dirty (2 messages, latest: Mar 26 2024 at 16:46)
- pretty print bindings in LaTeX (1 message, latest: Feb 23 2024 at 22:39)
- BST_Demo.thy (4 messages, latest: Jan 21 2024 at 11:59)
- Generalizing constants (3 messages, latest: Jan 05 2024 at 21:52)
- Tactic is repeated forever (20 messages, latest: Jan 05 2024 at 19:20)
- Detect Mutual Recursion (1 message, latest: Dec 06 2023 at 11:24)
- Info of primrec (3 messages, latest: Nov 15 2023 at 21:00)
- Functions Retrieving and Printing Proof State (6 messages, latest: Nov 14 2023 at 16:34)
- Automatic tactic for timing functions (3 messages, latest: Nov 08 2023 at 15:12)
- New Environment Variable (11 messages, latest: Oct 23 2023 at 06:51)
- Markup for arguments to custom commands (22 messages, latest: Oct 04 2023 at 09:36)
- "No content for theory certificate" for local propositions (2 messages, latest: Sep 20 2023 at 15:57)
- Toplevel macros (1 message, latest: Sep 01 2023 at 06:26)
- Parse AST translation patterns (1 message, latest: Aug 08 2023 at 06:05)
- Structural composition vs. terminal proof (7 messages, latest: Aug 08 2023 at 06:02)
- Change theory data in proof (9 messages, latest: May 02 2023 at 05:21)
- Pattern matching goals (14 messages, latest: Apr 21 2023 at 13:10)
- Equality in commutative monoids (8 messages, latest: Apr 21 2023 at 11:08)
- Isar Virtual Machine (3 messages, latest: Mar 29 2023 at 14:11)
- Folding definitions (2 messages, latest: Mar 27 2023 at 12:00)
- HOL Conversions (4 messages, latest: Mar 20 2023 at 10:15)
- Method.text vs. Method.method (9 messages, latest: Mar 14 2023 at 11:36)
- Registering conversions with simp (12 messages, latest: Mar 07 2023 at 09:57)
- Test for equality-by-simplification in ML (4 messages, latest: Mar 04 2023 at 06:04)
- isabelle (2 messages, latest: Mar 02 2023 at 13:52)
- type variable in datatype definition (3 messages, latest: Nov 29 2022 at 05:26)
- how to instantiate a schematic variable of a theorem? (4 messages, latest: Sep 19 2022 at 13:46)
- ✔ Do not note function theorems (2 messages, latest: Sep 17 2022 at 15:25)
- Do not note function theorems (2 messages, latest: Sep 17 2022 at 12:55)
- Isabelle Console seL4 (1 message, latest: Sep 15 2022 at 01:02)
- Discharge a goal using simplifier in ML (5 messages, latest: Sep 10 2022 at 15:27)
- Updating Isabelle/ML tutorial? (12 messages, latest: Sep 02 2022 at 08:33)
- Pending sort hypothesis with definition (1 message, latest: Jul 10 2022 at 09:12)
- bstring & xstring (9 messages, latest: May 22 2022 at 11:40)
- stream events (3 messages, latest: May 08 2022 at 15:56)
- ✔ Using facts proved in Isabelle/ML (3 messages, latest: Apr 28 2022 at 08:55)
- ✔ Solving a list of trivial goals (5 messages, latest: Apr 24 2022 at 16:42)
- print proof states (2 messages, latest: Apr 22 2022 at 07:00)
- printing proof terms (3 messages, latest: Apr 19 2022 at 17:32)
- syntax engine (1 message, latest: Jan 27 2022 at 14:23)
- ✔ combine premises in goal (19 messages, latest: Jan 24 2022 at 07:59)
- Understanding local theories (3 messages, latest: Jan 19 2022 at 17:24)
- ✔ Generating proof outlines (3 messages, latest: Dec 10 2021 at 17:33)
- ✔ Load ML files from other Sessions (6 messages, latest: Dec 03 2021 at 22:04)
- all theorems introduced in a theory (2 messages, latest: Dec 02 2021 at 09:08)
- term export argument in `Assumption.export` (6 messages, latest: Nov 26 2021 at 14:18)
- Full name of binding (3 messages, latest: Nov 03 2021 at 20:44)
- Differentiate hyps from context (2 messages, latest: Sep 30 2021 at 16:10)
- antiquotation embedded (1 message, latest: Sep 30 2021 at 13:07)
- Instantiating a theorem based on matching result (8 messages, latest: Sep 21 2021 at 06:53)
- ✔ Construct type application with unification (9 messages, latest: Sep 15 2021 at 13:40)
- PHOAS (4 messages, latest: Sep 01 2021 at 16:33)
- ✔ wrong unifier: meta variables of function types (2 messages, latest: Sep 01 2021 at 13:11)
- Exception in COMP (3 messages, latest: Aug 24 2021 at 19:53)
- Interface between Isabelle/ML and regular Isabelle (2 messages, latest: Jul 09 2021 at 19:24)
- AutoCorres (1 message, latest: Jul 02 2021 at 02:08)
- stack trace for exceptions (5 messages, latest: Jul 01 2021 at 13:52)
- Active Areas (8 messages, latest: Jun 28 2021 at 14:29)
- Unification issues with OF (8 messages, latest: Jun 18 2021 at 10:00)
- Forall introduction? (3 messages, latest: Jun 16 2021 at 19:49)
- Writing to file for logging (1 message, latest: Apr 26 2021 at 08:37)
- Illegal fixed variable error (1 message, latest: Apr 23 2021 at 15:49)
- Installation problem (3 messages, latest: Apr 10 2021 at 14:09)
- Fast Instantiation Method (1 message, latest: Sep 12 2020 at 08:39)
- Match subterms (1 message, latest: Oct 14 2019 at 10:34)
Last updated: Sep 15 2026 at 09:19 UTC