Stream: Beginner Questions

Topics:

• ✔ Why is this not working? (25 messages, latest: Jul 15 2026 at 15:04)
• Correct antiquotation when in draft and non-draft sessions (5 messages, latest: Jun 22 2026 at 10:45)
• ✔ Run two isabelle clients from the same server instance (4 messages, latest: Jun 19 2026 at 09:42)
• Contributing to Isabelle/jEdit (15 messages, latest: Jun 17 2026 at 13:07)
• Building my own deductive system. (1 message, latest: Jun 16 2026 at 08:18)
• ✔ workflow? (1 message, latest: Jun 13 2026 at 00:18)
• ✔ trace decomposition (2 messages, latest: Jun 12 2026 at 04:35)
• trace decomposition (1 message, latest: Jun 11 2026 at 09:37)
• Can't reopen Isabelle/jEdit on Windows 10 (1 message, latest: Jun 04 2026 at 07:18)
• How can I build the documentation for AutoCorres2? (2 messages, latest: May 26 2026 at 10:23)
• Embeddings in Pure w/o axiomatizations? (7 messages, latest: May 24 2026 at 12:22)
• workflow? (8 messages, latest: May 22 2026 at 11:03)
• Video Game Verification (6 messages, latest: May 15 2026 at 09:09)
• How to disable veriT (10 messages, latest: May 14 2026 at 23:11)
• is there a way to autoformat code (5 messages, latest: May 08 2026 at 15:51)
• SMT timeout issues (12 messages, latest: May 06 2026 at 18:12)
• local theorems get pulled from locale instead of class (4 messages, latest: May 06 2026 at 14:27)
• Getting value of a configuration parameter (17 messages, latest: May 06 2026 at 12:39)
• ✔ Annotating type parameters in a typedef (1 message, latest: May 04 2026 at 23:17)
• ✔ Unable to apply rule (1 message, latest: May 04 2026 at 22:35)
• Unable to apply rule (2 messages, latest: May 04 2026 at 08:38)
• Annotating type parameters in a typedef (3 messages, latest: May 01 2026 at 19:44)
• ✔ quotes versus angle brackets (3 messages, latest: Apr 24 2026 at 17:16)
• ✔ How can I shorten this simple Isar proof? (19 messages, latest: Apr 23 2026 at 21:45)
• Why have object logic forall? (5 messages, latest: Apr 23 2026 at 09:52)
• Abbreviation within an Isar proof (7 messages, latest: Apr 17 2026 at 14:49)
• ✔ Abbreviations do not contract (no locales though) (9 messages, latest: Apr 17 2026 at 03:37)
• Isabelle graph browser (11 messages, latest: Apr 15 2026 at 08:32)
• Abbreviations do not contract (no locales though) (6 messages, latest: Apr 13 2026 at 05:02)
• ✔ Type unification failure in locale (2 messages, latest: Apr 10 2026 at 11:05)
• Type unification failure in locale (24 messages, latest: Apr 09 2026 at 11:19)
• ✔ why does this proof fail when starting from an assumption? (5 messages, latest: Apr 08 2026 at 16:28)
• ✔ can't get congruence axiom to type check (1 message, latest: Apr 08 2026 at 13:21)
• can't get congruence axiom to type check (16 messages, latest: Apr 08 2026 at 07:34)
• ✔ why can't auto prove this statement, though blast can? (10 messages, latest: Mar 29 2026 at 11:55)
• ✔ can't finish proof by contradiction (4 messages, latest: Mar 29 2026 at 10:24)
• ✔ speeding up autocomplete? (12 messages, latest: Mar 28 2026 at 19:31)
• ✔ why doesn't "auto simp add:" work in this proof? (2 messages, latest: Mar 28 2026 at 14:13)
• why doesn't "auto simp add:" work in this proof? (6 messages, latest: Mar 28 2026 at 12:42)
• quotes versus angle brackets (5 messages, latest: Mar 28 2026 at 08:28)
• incomplete subproofs (6 messages, latest: Mar 27 2026 at 05:55)
• ✔ proof by class inheritance (2 messages, latest: Mar 26 2026 at 08:10)
• proof by class inheritance (5 messages, latest: Mar 24 2026 at 11:38)
• ✔ How to show active assumptions? (2 messages, latest: Mar 22 2026 at 06:46)
• How to show active assumptions? (2 messages, latest: Mar 21 2026 at 16:52)
• ✔ How can I invoke Sledgehammer to finish an induction pr... (5 messages, latest: Mar 21 2026 at 12:57)
• How can I invoke Sledgehammer to finish an induction proof? (1 message, latest: Mar 21 2026 at 11:59)
• Caching theorems (32 messages, latest: Mar 20 2026 at 19:13)
• ✔ Backwards compatibility (1 message, latest: Mar 20 2026 at 18:05)
• ✔ meaning of [type, type] in Pure metalogic? (1 message, latest: Mar 17 2026 at 11:13)
• meaning of [type, type] in Pure metalogic? (7 messages, latest: Mar 15 2026 at 14:25)
• ✔ when defining HOL, how can I cause λx.x to be a formula? (3 messages, latest: Mar 15 2026 at 12:28)
• BNF for ('a => 'b) => 'c with live 'a, 'c - possible? (13 messages, latest: Mar 02 2026 at 22:28)
• ✔ Trouble transferring relation predicates (1 message, latest: Mar 02 2026 at 22:27)
• Trouble transferring relation predicates (1 message, latest: Feb 27 2026 at 18:29)
• ✔ Calculation proofs have unintuitive behavior (2 messages, latest: Feb 24 2026 at 19:44)
• Calculation proofs have unintuitive behavior (11 messages, latest: Feb 24 2026 at 12:48)
• Adding more symbols to Isabelle-UTF8 (7 messages, latest: Feb 20 2026 at 15:13)
• Setting up Isabelle/VSCode (21 messages, latest: Feb 16 2026 at 14:39)
• Backwards compatibility (5 messages, latest: Feb 15 2026 at 08:52)
• How do I show a proof tree for an existing proof? (3 messages, latest: Feb 14 2026 at 20:13)
• Proving implications (7 messages, latest: Feb 13 2026 at 20:04)
• Induction on nonempty lists (12 messages, latest: Feb 06 2026 at 13:00)
• Making the fun package support recursion through datatypes (1 message, latest: Jan 29 2026 at 10:56)
• Two remaining errors in my Isabelle theory – need help under (1 message, latest: Jan 28 2026 at 05:39)
• Help needed: Broken build after Unicode errors in prime numb (2 messages, latest: Jan 27 2026 at 11:27)
• Bug report: Isabelle 2025-2 crash (3 messages, latest: Jan 26 2026 at 09:02)
• Code generation from locale interpretations within locale (6 messages, latest: Jan 21 2026 at 13:18)
• Problem with syntax (2 messages, latest: Jan 01 2026 at 17:54)
• Changing text colors in Isabelle/jEdit (3 messages, latest: Dec 19 2025 at 01:35)
• How can I get an uniform dark theme in jEdit? (11 messages, latest: Dec 17 2025 at 05:50)
• Recommended learning material (2 messages, latest: Dec 13 2025 at 02:59)
• PolyML Lexer (5 messages, latest: Dec 09 2025 at 03:29)
• Code printing underscores (3 messages, latest: Dec 06 2025 at 07:51)
• Recommended interface (3 messages, latest: Dec 04 2025 at 01:37)
• "Bad name" when defining a datatype (2 messages, latest: Nov 30 2025 at 02:53)
• Cloning the development repository (6 messages, latest: Nov 29 2025 at 22:44)
• Defining abstract Frechet derivative (9 messages, latest: Nov 26 2025 at 16:11)
• Hard time proving a simple lemma (4 messages, latest: Nov 26 2025 at 15:30)
• Automation breaks when swapping arguments (9 messages, latest: Nov 20 2025 at 06:15)
• Using a heap image (10 messages, latest: Nov 17 2025 at 21:00)
• proving an obvious statement (3 messages, latest: Nov 09 2025 at 20:09)
• Rewrting `subgoal_tac` in Isar (4 messages, latest: Oct 30 2025 at 01:37)
• Mixfix notation (3 messages, latest: Oct 29 2025 at 01:21)
• Defining automorphisms (11 messages, latest: Oct 27 2025 at 22:52)
• Quotient involving real^3 (5 messages, latest: Oct 09 2025 at 15:48)
• Basic facts about Cauchy sequences (8 messages, latest: Oct 08 2025 at 18:27)
• Pronunciation (4 messages, latest: Sep 26 2025 at 02:13)
• Set containment (5 messages, latest: Sep 22 2025 at 19:48)
• Oddity with records and locales (7 messages, latest: Sep 20 2025 at 15:28)
• Export files from session database exports (1 message, latest: Sep 18 2025 at 15:02)
• Just a small stylistic question about trivial proofs (6 messages, latest: Sep 17 2025 at 11:44)
• Simple Number theory proof (3 messages, latest: Aug 31 2025 at 22:12)
• Imports of HOL-Analysis not working after restart (5 messages, latest: Aug 04 2025 at 19:14)
• Help with syntax error. (3 messages, latest: Jul 30 2025 at 20:28)
• Understanding a particular instance of the induction method (2 messages, latest: Jul 25 2025 at 11:25)
• quotients and partial equivalence relations (3 messages, latest: Jul 21 2025 at 19:42)
• changelog for the documentation? (2 messages, latest: Jul 21 2025 at 07:55)
• Making sense out of the sessions library (8 messages, latest: Jul 21 2025 at 04:35)
• Defining a function on a datatype (9 messages, latest: Jul 14 2025 at 21:46)
• Quotient Basics and warnings (8 messages, latest: Jul 14 2025 at 20:19)
• Cardinality and indicator functions (11 messages, latest: Jul 08 2025 at 18:13)
• Notation for summation (4 messages, latest: Jul 08 2025 at 09:53)
• I don't know how to prove this simple lemma. (13 messages, latest: Jun 27 2025 at 09:24)
• obtaining elements of a small set (8 messages, latest: Jun 24 2025 at 13:39)
• Building and using HOL-Analysis (7 messages, latest: Jun 20 2025 at 20:24)
• intro! and elim! (5 messages, latest: Jun 14 2025 at 15:48)
• Why does "TERM _" appear. (4 messages, latest: Jun 13 2025 at 17:32)
• Stylistic choice, rule vs. erule (5 messages, latest: Jun 12 2025 at 14:22)
• What AFP version/s work for a given Isabelle version? (15 messages, latest: Jun 12 2025 at 01:22)
• Equation is redundant (covered by preceding clauses) (3 messages, latest: Jun 04 2025 at 12:41)
• Proving termination of function, if arguments well-formed (9 messages, latest: Jun 03 2025 at 15:56)
• Implicit universal quantification? (2 messages, latest: Jun 02 2025 at 09:37)
• Case-based proofs (3 messages, latest: May 30 2025 at 15:28)
• "infix" notation in a definition (7 messages, latest: May 28 2025 at 12:00)
• Proving things about a definition of a record (1 message, latest: May 28 2025 at 01:09)
• Isabelle shutting down on startup (8 messages, latest: May 21 2025 at 12:31)
• "house" character - what's the meaning? (6 messages, latest: May 14 2025 at 11:52)
• Fix some parameters in a locale (6 messages, latest: May 12 2025 at 07:21)
• "It suffices to show..." (8 messages, latest: May 11 2025 at 14:16)
• Isabelle/Pure: forbid a Prop from having a quantifier (5 messages, latest: May 05 2025 at 12:13)
• Isabelle's build error (8 messages, latest: May 02 2025 at 12:38)
• Why are these lemmas different and not legal? (9 messages, latest: May 02 2025 at 04:43)
• generic-length uncurrying function (9 messages, latest: Apr 30 2025 at 17:02)
• Proof obligation generated by obtain (4 messages, latest: Apr 25 2025 at 10:46)
• Prevent free variables in formula (1 message, latest: Apr 22 2025 at 15:48)
• Source-code definition of const (1 message, latest: Apr 20 2025 at 14:51)
• Batch-mode proof output for app + smt crash on macOS (17 messages, latest: Apr 11 2025 at 15:00)
• inductive definition fails (12 messages, latest: Apr 07 2025 at 14:03)
• Source for a term (5 messages, latest: Apr 01 2025 at 15:37)
• Use of `\<open>` (11 messages, latest: Mar 31 2025 at 19:50)
• Is it me or does isabelle slows do after running fo a while? (8 messages, latest: Mar 27 2025 at 14:58)
• Additional type variable(s) in specification: CKI combinator (9 messages, latest: Mar 24 2025 at 19:46)
• stubborn environment variable (20 messages, latest: Mar 24 2025 at 12:19)
• Support of Isabelle VScode extension for latest vscode (10 messages, latest: Mar 24 2025 at 10:13)
• Inner lexical error ? (5 messages, latest: Mar 21 2025 at 07:41)
• ML in an Isabelle theory (1 message, latest: Mar 21 2025 at 04:08)
• nothing known about theory (6 messages, latest: Mar 19 2025 at 07:56)
• Function termination proof extremely slow (26 messages, latest: Mar 17 2025 at 13:10)
• Keyword colours (1 message, latest: Mar 15 2025 at 09:17)
• installing cvc5 (8 messages, latest: Mar 14 2025 at 00:55)
• Isabelle/jEdit Rebuilding Heap Every Time (6 messages, latest: Mar 10 2025 at 08:33)
• Isabelle in Batch mode (7 messages, latest: Mar 09 2025 at 06:21)
• Locale semantics (10 messages, latest: Mar 06 2025 at 19:50)
• Executing functions defined in locales (6 messages, latest: Mar 05 2025 at 12:23)
• String inequality with show (5 messages, latest: Mar 03 2025 at 16:18)
• Skolem confusion (7 messages, latest: Mar 02 2025 at 19:05)
• What is `notepad` (6 messages, latest: Mar 02 2025 at 15:05)
• Conditional split rules (4 messages, latest: Mar 01 2025 at 10:03)
• Locals and the "for" keyword (40 messages, latest: Feb 28 2025 at 18:08)
• Isabelle Keeps Rebuilding HOL (4 messages, latest: Feb 26 2025 at 12:43)
• Using an existence and uniqueness theorem to define a func. (4 messages, latest: Feb 24 2025 at 16:06)
• Simplification for `Max {a..<b}` (1 message, latest: Feb 23 2025 at 07:51)
• Using classes (15 messages, latest: Feb 21 2025 at 08:07)
• Unfold only one occurrence (2 messages, latest: Feb 21 2025 at 05:31)
• Other editors (15 messages, latest: Feb 18 2025 at 17:07)
• Old style datatypes (4 messages, latest: Feb 17 2025 at 16:02)
• A syntax doubt (13 messages, latest: Feb 17 2025 at 13:49)
• Working with "Least" for the towers of hanoi (4 messages, latest: Feb 16 2025 at 19:39)
• Mutual recursion (4 messages, latest: Feb 13 2025 at 18:51)
• Defining a class (4 messages, latest: Feb 13 2025 at 17:46)
• Defining equality for a datatype (4 messages, latest: Feb 13 2025 at 06:20)
• Missing theory context (4 messages, latest: Feb 12 2025 at 07:22)
• HOL-Algebra (5 messages, latest: Feb 10 2025 at 15:24)
• Defining a quotient in a locale (1 message, latest: Feb 10 2025 at 11:18)
• Picking corresponding values from zip lists (29 messages, latest: Feb 10 2025 at 09:07)
• Injective image of reflexive and transitive closure (34 messages, latest: Feb 09 2025 at 16:58)
• Why sledgehammer refuses to give me this? (14 messages, latest: Feb 08 2025 at 21:20)
• Not to expand abbreviation in proof state (20 messages, latest: Feb 07 2025 at 17:39)
• Choice operator on sets? (27 messages, latest: Feb 07 2025 at 15:51)
• How to use hide_cons for syntactic sugar? (1 message, latest: Feb 06 2025 at 20:34)
• infinite type 'a has an injection (nat * 'a) -> 'a (9 messages, latest: Feb 06 2025 at 13:25)
• Reuse/import notation from interpreted locale (2 messages, latest: Feb 06 2025 at 09:25)
• Isabelle Build Error: "Bad imports session" in ROOT file (2 messages, latest: Feb 06 2025 at 05:53)
• Latex for showing Isabelle input? (6 messages, latest: Feb 05 2025 at 18:55)
• Construction a set (7 messages, latest: Feb 05 2025 at 17:10)
• Proving map version of function (2 messages, latest: Feb 05 2025 at 15:45)
• Function gives the list [0,1,2,...,n] (10 messages, latest: Feb 04 2025 at 20:16)
• Struggling to prove accumulator function relation (2 messages, latest: Feb 04 2025 at 06:01)
• Riemann Integrals (6 messages, latest: Feb 02 2025 at 14:34)
• Editing a file without disabling navigation in other files (4 messages, latest: Feb 02 2025 at 12:44)
• Isabelle stuck while checking proof (5 messages, latest: Feb 02 2025 at 10:34)
• Least vs LEAST vs Inf vs Min (11 messages, latest: Jan 31 2025 at 16:04)
• Defining inductive predicate: fun vs primrec vs inductive? (44 messages, latest: Jan 30 2025 at 18:34)
• Adding to a fact set (4 messages, latest: Jan 29 2025 at 11:05)
• Using "presume" (3 messages, latest: Jan 28 2025 at 16:21)
• Convention for dealing with definition with multiple clauses (22 messages, latest: Jan 27 2025 at 19:02)
• Struggling with a trivial set equality (8 messages, latest: Jan 15 2025 at 10:01)
• Using "^" in cring (4 messages, latest: Jan 14 2025 at 14:55)
• Applying cases for nested patterns without subgoal (3 messages, latest: Jan 10 2025 at 18:06)
• Syntactic Sugar for a Logic (3 messages, latest: Jan 05 2025 at 17:33)
• Locale interpretation duplicate fact declaration (3 messages, latest: Jan 05 2025 at 16:36)
• Proving facts about nat by enumerating? (5 messages, latest: Dec 31 2024 at 16:30)
• How to prove a simple cases of (4 messages, latest: Dec 30 2024 at 12:04)
• Starting a induction with in a larger proof (14 messages, latest: Dec 25 2024 at 21:47)
• How is this schematic goal provable by assumption? (2 messages, latest: Dec 22 2024 at 11:20)
• Functions that applies to theorems (12 messages, latest: Dec 20 2024 at 19:13)
• What about a 'suffices to show' Isar keyword? (7 messages, latest: Dec 19 2024 at 19:17)
• What are some good AFP entries for beginners? (11 messages, latest: Dec 19 2024 at 19:12)
• Converting facts from pattern matching single-constructors (12 messages, latest: Dec 19 2024 at 14:58)
• Why is this goal provable by assumption? (5 messages, latest: Dec 18 2024 at 18:07)
• Do we have functions transforming thms using convs? (7 messages, latest: Dec 14 2024 at 18:50)
• Do we have something like "simp once"/"unfolding once"? (11 messages, latest: Dec 14 2024 at 16:03)
• Usage of Inf/LEAST (17 messages, latest: Dec 14 2024 at 12:29)
• Improving Binary Decision Diagram Proof (6 messages, latest: Dec 13 2024 at 16:33)
• Clash of types error in a definition of a construction (10 messages, latest: Dec 11 2024 at 23:53)
• Why doesn't this proof work without rule_format? (15 messages, latest: Dec 11 2024 at 14:40)
• Defining the range in a locale based on a record (15 messages, latest: Dec 11 2024 at 05:05)
• Usual track to simplify this goal (18 messages, latest: Dec 10 2024 at 19:59)
• What is wrong with the following inductive_set declaration? (19 messages, latest: Dec 10 2024 at 14:11)
• Usage of ex_neg_all_pos (33 messages, latest: Dec 09 2024 at 09:11)
• Isabelle-dev fails to build HOL on macs without rosetta? (1 message, latest: Dec 08 2024 at 21:28)
• Why unfolding Bex_def, bex_triv does not work here? (35 messages, latest: Dec 08 2024 at 06:41)
• Defining custom case rules? (4 messages, latest: Dec 05 2024 at 06:10)
• Many hide_fact and hide_const stmnts required, ok for AFP? (4 messages, latest: Dec 02 2024 at 22:37)
• Does there exists a notion of $$A\times ...\times A$$? (3 messages, latest: Dec 02 2024 at 10:36)
• Using surjection to prove finiteness (6 messages, latest: Nov 30 2024 at 09:40)
• when to use ⋀. vs ∀. (11 messages, latest: Nov 20 2024 at 14:56)
• Calculation of Lebesgue-Stieltjes Integral (12 messages, latest: Nov 19 2024 at 12:46)
• Cannot find a constant "count" (5 messages, latest: Nov 17 2024 at 20:41)
• Commenting on a piece of my formalisation (1 message, latest: Nov 17 2024 at 18:03)
• Creating clickable files that are reference by a file. (8 messages, latest: Nov 11 2024 at 09:39)
• Stating a theorem so "unfolding" automatically split (34 messages, latest: Nov 07 2024 at 12:28)
• Simple inequality (5 messages, latest: Nov 06 2024 at 15:46)
• Using "OF" regardless of the order (8 messages, latest: Nov 05 2024 at 12:11)
• Sledgehammer proof found quickly but not work (76 messages, latest: Nov 04 2024 at 10:04)
• Colon illegal in Path on Windows with vscodium (11 messages, latest: Nov 04 2024 at 00:30)
• Stating a theorem like the "simps" (3 messages, latest: Nov 01 2024 at 10:47)
• Automatic proof obligations from rule pattern matching (10 messages, latest: Oct 31 2024 at 18:58)
• Syntax for proving termination of this recursive predicate (32 messages, latest: Oct 31 2024 at 14:24)
• How to stop a running "try" process? (4 messages, latest: Oct 31 2024 at 12:17)
• Let statement seems to complicate proofs (7 messages, latest: Oct 31 2024 at 07:04)
• autocorres for starters (23 messages, latest: Oct 23 2024 at 00:04)
• Order of conjuncts of induction principle (12 messages, latest: Oct 21 2024 at 05:55)
• Display all the founded theorems (26 messages, latest: Oct 21 2024 at 05:40)
• subsetI followed by an induction (9 messages, latest: Oct 20 2024 at 14:10)
• Conclusion of introduction rule inductive predicate (6 messages, latest: Oct 20 2024 at 07:14)
• Lemmas from a definition by constructors give a contraction (3 messages, latest: Oct 19 2024 at 04:10)
• "size_list" in a termination proof (14 messages, latest: Oct 14 2024 at 07:12)
• simps changes to psimps after editing (16 messages, latest: Oct 13 2024 at 08:25)
• Unexpected generated termination goal (21 messages, latest: Oct 12 2024 at 15:33)
• Convertion about pairs (components specified/unspecified) (21 messages, latest: Oct 12 2024 at 06:30)
• Isabelle cannot recognize the type of "fix" (18 messages, latest: Oct 12 2024 at 06:13)
• new to isssable from lean where to get started (2 messages, latest: Oct 12 2024 at 04:24)
• Multiple instances of the same locale in one theorem (15 messages, latest: Oct 07 2024 at 07:43)
• Ill-formed introduction rule (2 messages, latest: Oct 04 2024 at 04:11)
• Default proof method creates an unprovable goal (9 messages, latest: Oct 02 2024 at 14:45)
• Construct a term of types constructed using type_definition (9 messages, latest: Oct 01 2024 at 15:02)
• Why sledgehammer's takes so long for this? (1 message, latest: Sep 29 2024 at 08:43)
• Why I cannot assume one conjunct only after (elim conjE)? (14 messages, latest: Sep 29 2024 at 07:55)
• Is there already a theory for n-ary relation for n > 2? (16 messages, latest: Sep 26 2024 at 15:39)
• Is there a better way to deal with chained equations? (4 messages, latest: Sep 24 2024 at 23:43)
• induction rule from `fun` (4 messages, latest: Sep 24 2024 at 19:01)
• Setup subgoals after tactic application in Isar (138 messages, latest: Sep 23 2024 at 09:16)
• Error in prog-prove Exercise 3.4 (3 messages, latest: Sep 23 2024 at 06:32)
• Manual termination proof and congruence rules (2 messages, latest: Sep 19 2024 at 17:58)
• Fixing the record scheme to a particular type (1 message, latest: Sep 17 2024 at 18:27)
• Applying the results obtained by "try" (14 messages, latest: Sep 17 2024 at 18:00)
• "apply" after "proof" (6 messages, latest: Sep 17 2024 at 13:19)
• Why is this syntax error have ... by have ...by (14 messages, latest: Sep 17 2024 at 11:40)
• Avoid getting this term mis-type-inferenced (28 messages, latest: Sep 16 2024 at 08:13)
• How to manipulate theorems using functions (ML functions)? (4 messages, latest: Sep 14 2024 at 09:51)
• What to type to help sledgehammer solving this goal? (21 messages, latest: Sep 14 2024 at 06:22)
• Why it seems like Isabelle does not get my definition (50 messages, latest: Sep 13 2024 at 17:10)
• Treatment of this pattern (11 messages, latest: Sep 13 2024 at 13:58)
• Set Comprehension in FSet (6 messages, latest: Sep 13 2024 at 10:02)
• Splitting disjunction (seems to be syntax error) (30 messages, latest: Sep 13 2024 at 05:08)
• Quote generated variable name: (9 messages, latest: Sep 12 2024 at 18:21)
• Why this goal cannot be solved automatically? (21 messages, latest: Sep 12 2024 at 18:04)
• Extending/Restricting Sub-record type (instead of fields) (12 messages, latest: Sep 12 2024 at 17:42)
• Successful attempt to solve goal/Failed to finish proof (43 messages, latest: Sep 12 2024 at 14:09)
• "iff" definitions with meta-equations? (7 messages, latest: Sep 12 2024 at 09:37)
• Outer syntax error: proposition expected (4 messages, latest: Sep 12 2024 at 08:40)
• Viewing a theorem/rule in the interactive window (7 messages, latest: Sep 12 2024 at 05:44)
• `'a => bool` vs `'a set` (10 messages, latest: Sep 11 2024 at 15:55)
• triple dot for chains of >= inequalities (10 messages, latest: Sep 09 2024 at 15:38)
• Sledgehammer Windows Issues (7 messages, latest: Sep 06 2024 at 13:45)
• AFP Entry Preparation (8 messages, latest: Sep 06 2024 at 03:07)
• Does Isabelle run natively on Apple Silicon (4 messages, latest: Sep 02 2024 at 11:02)
• Isabelle prover inactive (12 messages, latest: Aug 30 2024 at 16:29)
• Relaxing subterms inside inequality (13 messages, latest: Aug 30 2024 at 10:49)
• parsing (6 messages, latest: Aug 29 2024 at 19:10)
• Is it possible to use Isabelle without Java? (4 messages, latest: Aug 26 2024 at 09:18)
• Induction and Contradiction Proofs (10 messages, latest: Aug 23 2024 at 06:04)
• error bad directory (2 messages, latest: Aug 20 2024 at 18:58)
• The different between Lean and Isabelle (15 messages, latest: Aug 14 2024 at 15:37)
• Generated code slower than "value" command (5 messages, latest: Aug 01 2024 at 08:41)
• colors (2 messages, latest: Jul 29 2024 at 21:05)
• Sledgehammer: > 1.0 s, timed out (11 messages, latest: Jul 26 2024 at 15:35)
• Eisbach - (2 messages, latest: Jul 22 2024 at 22:00)
• Semantics of bit vector multiplication. (9 messages, latest: Jul 16 2024 at 18:18)
• Windows eprover Memory Bug in Isabelle2024 (2 messages, latest: Jul 13 2024 at 15:49)
• Evaluation speed (12 messages, latest: Jul 10 2024 at 20:14)
• Is it a new semantics for Isabelle's metatheory? (5 messages, latest: Jul 09 2024 at 17:53)
• Locale usage: Clash of types "_ set" and "_ itself" (4 messages, latest: Jul 03 2024 at 14:02)
• local assumptions vs simp add (2 messages, latest: Jun 29 2024 at 07:44)
• Defining a complicated macros (2 messages, latest: Jun 27 2024 at 04:54)
• Datatype issuue -Greedy Algorithm of Greedoids (7 messages, latest: Jun 22 2024 at 13:08)
• Using let-defined names in structured proofs (1 message, latest: Jun 18 2024 at 07:45)
• Sledgehammer: naming a theory (3 messages, latest: Jun 15 2024 at 18:35)
• "using assms" (6 messages, latest: Jun 13 2024 at 16:07)
• Square root function (18 messages, latest: Jun 10 2024 at 15:01)
• A simple theorem about lists (5 messages, latest: Jun 09 2024 at 10:00)
• How to do induction on set? (9 messages, latest: Jun 08 2024 at 18:07)
• Proving Inequality of Collections.Collections.hm (6 messages, latest: Jun 03 2024 at 14:43)
• Proving an Inequality (8 messages, latest: May 31 2024 at 18:48)
• Proof by inversion on mutual inductively defined proposition (3 messages, latest: May 31 2024 at 14:41)
• a lemma proof (1 message, latest: May 28 2024 at 17:39)
• Use polynomial or matrix (7 messages, latest: May 28 2024 at 16:51)
• rendered version of html documentation (2 messages, latest: May 14 2024 at 10:03)
• Unification for encrypting (elgamal, game based crypto) 1 (11 messages, latest: May 13 2024 at 14:35)
• Parser for Isabelle (29 messages, latest: May 12 2024 at 01:39)
• proving lemmas on the end of a list (8 messages, latest: May 10 2024 at 08:51)
• Isabelle build fails with "malformed command syntax" (10 messages, latest: May 07 2024 at 16:51)
• Undefined type names and failed type unification (11 messages, latest: May 06 2024 at 23:06)
• How to search for functions using find_theorems (4 messages, latest: May 06 2024 at 08:53)
• TYPE and itself (12 messages, latest: May 03 2024 at 14:47)
• Additional type variable(s) in locale specification (3 messages, latest: May 03 2024 at 12:56)
• Undoing `dest / intro` declarations (3 messages, latest: May 03 2024 at 08:46)
• Failed to refined pending goal when implementing class (6 messages, latest: May 02 2024 at 08:15)
• Proof by cases of map on which list element (11 messages, latest: May 02 2024 at 04:49)
• A "cases"-like construction that works through a small set (13 messages, latest: May 01 2024 at 16:43)
• Intro and elimination rules (7 messages, latest: May 01 2024 at 05:36)
• Extract explicit value from Isabelle proof (3 messages, latest: Apr 27 2024 at 21:03)
• goal in context cannot be proved (11 messages, latest: Apr 25 2024 at 11:51)
• Checking proof without jEdit (20 messages, latest: Apr 24 2024 at 05:51)
• Split if/case in induction rule (5 messages, latest: Apr 23 2024 at 21:36)
• how to adjust inductive hypothesis (13 messages, latest: Apr 19 2024 at 13:58)
• Max in a list (23 messages, latest: Apr 16 2024 at 10:05)
• Malfunction or faulty operation? (12 messages, latest: Apr 15 2024 at 21:13)
• html manipulation (5 messages, latest: Apr 15 2024 at 11:21)
• using/unfolding assms (46 messages, latest: Apr 12 2024 at 01:18)
• induction rule for odd numbers (4 messages, latest: Apr 11 2024 at 17:36)
• Using Isabelle as an automated testing tool (3 messages, latest: Apr 11 2024 at 12:30)
• why can't I use two induction rules at the same time (14 messages, latest: Apr 10 2024 at 12:54)
• Proof of recursive function (30 messages, latest: Apr 09 2024 at 19:57)
• Color coding (2 messages, latest: Apr 09 2024 at 11:53)
• how to print the inductive hypothesis (2 messages, latest: Apr 08 2024 at 15:37)
• Executing Imperative-HOL (6 messages, latest: Apr 05 2024 at 12:53)
• Why can't I unfold definitions from inside locales? (4 messages, latest: Apr 04 2024 at 19:54)
• Lemma usage in other lemmas (11 messages, latest: Apr 03 2024 at 16:03)
• Is it possible to expose sublocale namespace? (3 messages, latest: Apr 01 2024 at 20:00)
• What to do when ?this and the goal are identical (3 messages, latest: Apr 01 2024 at 13:21)
• How to structure proofs with inductive sets with parameters? (2 messages, latest: Mar 31 2024 at 20:50)
• subcases in cases (2 messages, latest: Mar 26 2024 at 10:41)
• Prevent safe from splitting tuples (1 message, latest: Mar 26 2024 at 10:23)
• Grammar (7 messages, latest: Mar 25 2024 at 20:01)
• using lemma in later proof (5 messages, latest: Mar 25 2024 at 18:09)
• recursive function proving (5 messages, latest: Mar 25 2024 at 10:21)
• Shorthand to split an assumed conjunction (4 messages, latest: Mar 24 2024 at 10:14)
• Derived "False" from these facts alone: ... using sledgeham (12 messages, latest: Mar 23 2024 at 14:17)
• Proof of monotonicity for `partial_function` (5 messages, latest: Mar 23 2024 at 12:35)
• How to structure sublocales for 'derived' objects? (12 messages, latest: Mar 20 2024 at 16:10)
• How to choose Isabelle/HOL's axiom system? (30 messages, latest: Mar 18 2024 at 16:49)
• Can't we make the following: (2 messages, latest: Mar 18 2024 at 09:34)
• no code equation (13 messages, latest: Mar 14 2024 at 12:02)
• A simple structural induction (5 messages, latest: Mar 12 2024 at 16:23)
• controlling quantification of induction (5 messages, latest: Mar 12 2024 at 12:41)
• Simple set proof (23 messages, latest: Mar 10 2024 at 17:12)
• how to prove below lemma (10 messages, latest: Mar 07 2024 at 15:25)
• Should I always bundle the data in a locale into a record? (4 messages, latest: Mar 01 2024 at 21:10)
• Question about non-terminating sledgehammer proofs (3 messages, latest: Feb 28 2024 at 10:22)
• apply a tactic to later subgoals (2 messages, latest: Feb 26 2024 at 03:40)
• Missing instruction for updating AFP component? (4 messages, latest: Feb 21 2024 at 06:50)
• Direct product of infinite family of groups (20 messages, latest: Feb 20 2024 at 11:54)
• how to write a function based on a lemma (2 messages, latest: Feb 19 2024 at 15:46)
• Multiple types of division for integers in the same Theory (6 messages, latest: Feb 16 2024 at 11:41)
• Proof using induction on list (41 messages, latest: Feb 16 2024 at 10:23)
• how to use well-founded induction (2 messages, latest: Feb 15 2024 at 16:22)
• Boolean algebras in the style of HOL-Algebra? (7 messages, latest: Feb 14 2024 at 18:05)
• Zero and Natural Numbers in Isabelle/HOL (3 messages, latest: Feb 14 2024 at 17:31)
• How to approach proof of this lemma? (8 messages, latest: Feb 12 2024 at 12:03)
• Override assumptions from superclass (2 messages, latest: Feb 11 2024 at 15:44)
• Best practices for implementing object logics (1 message, latest: Feb 10 2024 at 15:21)
• Naming facts in an Isar proof usable in subgoals (2 messages, latest: Feb 09 2024 at 09:11)
• Issue opening with prebuilt parent session image (23 messages, latest: Feb 08 2024 at 14:45)
• Making use of premises in Isar without "assumes" (4 messages, latest: Feb 08 2024 at 14:30)
• Finishing an Isar Proof (6 messages, latest: Feb 08 2024 at 01:36)
• Sledgehammer can't find agsyhol (6 messages, latest: Feb 07 2024 at 21:57)
• some confuse about induction (3 messages, latest: Feb 06 2024 at 20:58)
• how to take the union of the morphism sets of two categories (2 messages, latest: Feb 06 2024 at 20:07)
• Foldr invariant on permutations (20 messages, latest: Feb 06 2024 at 08:42)
• Isar proof of conjunctions not working (8 messages, latest: Feb 06 2024 at 01:44)
• termination proof on measure (10 messages, latest: Feb 05 2024 at 17:10)
• struggling with proving the simplest things (3 messages, latest: Feb 05 2024 at 06:11)
• can't instantiate quantifiers (9 messages, latest: Feb 02 2024 at 14:14)
• how to define a category using the category theory library (4 messages, latest: Feb 01 2024 at 14:32)
• Proof of List.fold (22 messages, latest: Feb 01 2024 at 14:08)
• stuck with proof (7 messages, latest: Jan 31 2024 at 11:25)
• how to define the quotient of a set (3 messages, latest: Jan 30 2024 at 11:46)
• Big Oh Basic Proof Failing: Type unification failed: No type (7 messages, latest: Jan 30 2024 at 04:21)
• Proofing measures with simp (8 messages, latest: Jan 27 2024 at 17:02)
• AFP installation on Mac (12 messages, latest: Jan 26 2024 at 12:06)
• Import breaks code generation (6 messages, latest: Jan 25 2024 at 13:06)
• Functions output (2 messages, latest: Jan 24 2024 at 09:18)
• Installation error (2 messages, latest: Jan 22 2024 at 19:00)
• Termination (9 messages, latest: Jan 19 2024 at 13:47)
• Isamode on Emacs (4 messages, latest: Jan 19 2024 at 05:58)
• Debug type requirements (4 messages, latest: Jan 17 2024 at 13:27)
• Code generation with compound abstract types (11 messages, latest: Jan 14 2024 at 14:46)
• Concrete Semantics Chapter 10_4 (1 message, latest: Jan 08 2024 at 21:17)
• Permutations (1 message, latest: Jan 08 2024 at 12:06)
• Nitpick? (5 messages, latest: Jan 07 2024 at 22:33)
• very new to isabelle, can't figure out why jeditor not work (3 messages, latest: Dec 30 2023 at 10:08)
• Brute Force Computation (8 messages, latest: Dec 26 2023 at 21:54)
• Dicts in Isabelle. (5 messages, latest: Dec 15 2023 at 21:10)
• Question about isabelle's class (3 messages, latest: Dec 15 2023 at 10:07)
• Bad context for command "definition" - using reuse state (9 messages, latest: Dec 14 2023 at 08:40)
• itself (4 messages, latest: Dec 13 2023 at 14:21)
• Would like to subscribe to Standard ML Zulip Chat (2 messages, latest: Dec 13 2023 at 04:56)
• No code equation for interpretation, unless it is global (1 message, latest: Dec 12 2023 at 15:46)
• Not an equation - Function (9 messages, latest: Dec 12 2023 at 14:49)
• Lists in Isabelle/HOL (3 messages, latest: Dec 11 2023 at 08:53)
• Coercion inference rat (6 messages, latest: Dec 08 2023 at 08:50)
• note in apply script (6 messages, latest: Dec 07 2023 at 16:21)
• smt tactic nondeterminism (3 messages, latest: Dec 07 2023 at 08:45)
• splitting case ... of ... (6 messages, latest: Dec 07 2023 at 01:08)
• Proofs by contradiction (3 messages, latest: Dec 05 2023 at 07:20)
• Wellsortedness error (11 messages, latest: Dec 04 2023 at 09:05)
• Compiling a .thy file? (7 messages, latest: Nov 30 2023 at 14:16)
• Make use of bracketed premises in Isar (9 messages, latest: Nov 23 2023 at 09:32)
• fine-grained single-step rewrites for both premises and goal (7 messages, latest: Nov 20 2023 at 21:33)
• substitution from assumptions, choosing which one you want (18 messages, latest: Nov 19 2023 at 12:25)
• Question on warning (3 messages, latest: Nov 17 2023 at 21:17)
• Is there a type for ranges of natural type ? (9 messages, latest: Nov 17 2023 at 16:11)
• refinement case assumotions in ISAP computation induction (4 messages, latest: Nov 17 2023 at 15:20)
• rule/assumption that do not unify schematic variables (4 messages, latest: Nov 15 2023 at 21:18)
• Unfolding definition for conclusion only (3 messages, latest: Nov 15 2023 at 19:20)
• Simplifying "(if 1 = 0 then P else Q)" to Q (3 messages, latest: Nov 14 2023 at 17:05)
• Unfolding definitions in locale (5 messages, latest: Nov 08 2023 at 12:57)
• Adding dependent types to Isabelle/HOL (12 messages, latest: Nov 07 2023 at 23:17)
• Resolve higher order assumptions in apply script (2 messages, latest: Nov 03 2023 at 12:05)
• Unfold definition for termination proof (9 messages, latest: Nov 03 2023 at 11:21)
• Generalizing some lemmas about vector spaces to modules (1 message, latest: Nov 02 2023 at 09:31)
• Compilation with MLton failed for Codegenerator_Test (3 messages, latest: Nov 02 2023 at 03:22)
• Sledgehammer and locales? (5 messages, latest: Oct 30 2023 at 15:30)
• Bundling data across multiple polymorphic types (3 messages, latest: Oct 30 2023 at 00:51)
• In locale, define things before locale ends (7 messages, latest: Oct 29 2023 at 18:03)
• Locale assumptions break my proof? (4 messages, latest: Oct 29 2023 at 02:13)
• Sledgehammer (smt verit) reconstruction failure (8 messages, latest: Oct 28 2023 at 15:28)
• Define a datatype from a given scope (6 messages, latest: Oct 25 2023 at 09:08)
• Access fixed constants from locale interpretation (6 messages, latest: Oct 18 2023 at 14:26)
• ML command to list/print lemmas proven in current theory (2 messages, latest: Oct 17 2023 at 05:54)
• Vscode (9 messages, latest: Oct 09 2023 at 07:05)
• Type Checking Error: Matrices (3 messages, latest: Oct 08 2023 at 22:56)
• countably infinite (4 messages, latest: Oct 05 2023 at 10:54)
• Achieving "Generic Type Classes" (5 messages, latest: Oct 04 2023 at 11:10)
• Lexicographic induction (17 messages, latest: Sep 29 2023 at 11:27)
• Code export with uncomputable branches (3 messages, latest: Sep 23 2023 at 08:14)
• Isabelle to XML (18 messages, latest: Sep 21 2023 at 12:23)
• Proof of mirrored binary trees (7 messages, latest: Sep 19 2023 at 20:46)
• Formalizing implicit assumption from pen and paper (17 messages, latest: Sep 19 2023 at 09:27)
• Concrete semantics theorem proving (4 messages, latest: Sep 17 2023 at 23:30)
• Instantiating typeclass on composite type (1 message, latest: Sep 14 2023 at 07:48)
• Forward fact resolution with an implication (8 messages, latest: Sep 13 2023 at 13:30)
• Malformed global fact: illegal fixed variable (5 messages, latest: Sep 13 2023 at 12:40)
• Why is `list_update_beyond` marked simp? (3 messages, latest: Sep 13 2023 at 07:17)
• Finite distribution (1 message, latest: Sep 11 2023 at 08:33)
• dest_Free error while interpreting statespace locale (3 messages, latest: Sep 08 2023 at 13:07)
• Navigation in finished theories (3 messages, latest: Sep 08 2023 at 12:23)
• dest_Free error while interpreting locale (1 message, latest: Sep 08 2023 at 12:15)
• Searching theorems with a particular attribute (9 messages, latest: Sep 05 2023 at 13:21)
• Typeclass instantiation within proof (12 messages, latest: Sep 04 2023 at 22:13)
• Mutual & partial recursion – Tactic failed (6 messages, latest: Sep 04 2023 at 09:35)
• Good Style Suggestion for Locales (4 messages, latest: Sep 03 2023 at 10:33)
• Additional type variable(s) in specification (5 messages, latest: Sep 01 2023 at 22:11)
• Timeout proof of False in empty file (2023 RC3) (7 messages, latest: Aug 31 2023 at 10:39)
• functions that may not terminate (23 messages, latest: Aug 30 2023 at 13:48)
• Sources for Isabelle knowledge (6 messages, latest: Aug 30 2023 at 08:04)
• Theories in subdirectories (3 messages, latest: Aug 28 2023 at 07:56)
• Isabelle VSCode (22 messages, latest: Aug 23 2023 at 19:21)
• Finding calculational algebraic proof (5 messages, latest: Aug 18 2023 at 18:47)
• Inductive set predicates not proven (9 messages, latest: Aug 16 2023 at 12:31)
• Failed to submit an AFP entry (5 messages, latest: Aug 10 2023 at 17:13)
• Datatype with label (5 messages, latest: Aug 10 2023 at 15:43)
• Finding "obvious" definitions and lemmas? (4 messages, latest: Aug 04 2023 at 09:43)
• well-founded order (1 message, latest: Aug 03 2023 at 17:29)
• Getting values out of a datatype (8 messages, latest: Aug 03 2023 at 13:40)
• Class constraints ignored in type synonym definition (7 messages, latest: Aug 03 2023 at 13:03)
• Concrete syntax for a type class symbol (10 messages, latest: Aug 02 2023 at 11:52)
• Undefined session (2 messages, latest: Aug 02 2023 at 10:44)
• prove {1::nat} <= {2} (17 messages, latest: Aug 01 2023 at 21:50)
• Proving == (9 messages, latest: Aug 01 2023 at 12:19)
• Understanding the automation in .. (2 messages, latest: Aug 01 2023 at 12:07)
• Question about fun extends to linorder (28 messages, latest: Jul 31 2023 at 20:33)
• Type class instantiation (8 messages, latest: Jul 31 2023 at 15:20)
• About the code generation- Wellsortedness error (7 messages, latest: Jul 31 2023 at 00:57)
• How to import the HOL theory to use (4 messages, latest: Jul 26 2023 at 16:41)
• How to handle assumptions? (7 messages, latest: Jul 26 2023 at 15:10)
• viewing a complicated proof state (5 messages, latest: Jul 26 2023 at 13:39)
• Understanding automation (5 messages, latest: Jul 26 2023 at 10:01)
• Why does map_t function fails (20 messages, latest: Jul 25 2023 at 17:43)
• local infix operator definition (9 messages, latest: Jul 23 2023 at 05:38)
• multiple "automatic" proof steps (7 messages, latest: Jul 20 2023 at 15:34)
• bug? (6 messages, latest: Jul 19 2023 at 14:15)
• Injective functions on large enums (7 messages, latest: Jul 19 2023 at 10:38)
• Creating slides with verbatim Isabelle content (2 messages, latest: Jul 19 2023 at 10:37)
• How to define an arbitrary predecate in Isabelle (2 messages, latest: Jul 18 2023 at 21:35)
• difference between `proof` and `proof -` (6 messages, latest: Jul 18 2023 at 14:56)
• Question about the type (8 messages, latest: Jul 16 2023 at 13:17)
• Arguments become invalid when transferred into new documents (10 messages, latest: Jul 13 2023 at 16:47)
• About AFP in Isabelle 2020 (14 messages, latest: Jul 09 2023 at 17:15)
• `experiment` bad context for (3 messages, latest: Jul 09 2023 at 14:50)
• Injectivity + finite equal sized sets implies surjectivity (3 messages, latest: Jul 08 2023 at 14:47)
• Proving the same statement with for all (4 messages, latest: Jul 07 2023 at 16:15)
• Conditions after the "for all" quantifier (6 messages, latest: Jul 06 2023 at 13:38)
• Arbitrary number of variables (7 messages, latest: Jul 05 2023 at 18:28)
• Using lemmas that assume a different type (6 messages, latest: Jul 04 2023 at 01:04)
• Transfer/Lifting problem with nested typedefs in record (1 message, latest: Jun 30 2023 at 13:59)
• Type cardinality (5 messages, latest: Jun 29 2023 at 08:54)
• Order-sorted algebra (1 message, latest: Jun 29 2023 at 07:13)
• Without loss of generality (7 messages, latest: Jun 27 2023 at 16:38)
• Vector (1 message, latest: Jun 27 2023 at 15:40)
• Compactness proof and model theory (21 messages, latest: Jun 27 2023 at 10:02)
• Reset jedit window settings? (13 messages, latest: Jun 24 2023 at 13:40)
• Weird induction scheme (5 messages, latest: Jun 23 2023 at 15:16)
• A style of stating a theorem (4 messages, latest: Jun 21 2023 at 14:06)
• Purple metis call (16 messages, latest: Jun 16 2023 at 08:05)
• Forward reasoning with equalities (8 messages, latest: Jun 15 2023 at 17:30)
• Searching functions (2 messages, latest: Jun 14 2023 at 15:19)
• jEdit reloading lib theories (9 messages, latest: Jun 13 2023 at 10:49)
• anonymous type conversion in proof state (5 messages, latest: Jun 13 2023 at 09:54)
• Question about the induct tactic (1 message, latest: Jun 12 2023 at 12:31)
• Using Akra_Bazzi (12 messages, latest: Jun 07 2023 at 19:07)
• Finding qualified name for const in scope (5 messages, latest: Jun 06 2023 at 23:03)
• Inner syntax error on decimal point (8 messages, latest: Jun 06 2023 at 22:54)
• Renaming of context elements / types in locales (1 message, latest: Jun 06 2023 at 09:53)
• Simplifier & meta All (10 messages, latest: Jun 06 2023 at 08:54)
• [TeX] File ended while scanning use of \next (1 message, latest: Jun 06 2023 at 08:46)
• How to prove the complement automaton in below way (13 messages, latest: Jun 05 2023 at 18:34)
• all errors from isabelle build (3 messages, latest: Jun 05 2023 at 11:38)
• (subst X; simp) vs (simp) (2 messages, latest: Jun 05 2023 at 05:24)
• Is it possible to create a typedef of a typedef? (2 messages, latest: Jun 04 2023 at 23:08)
• Latex Snippets Generation: colored keywords (1 message, latest: Jun 01 2023 at 13:52)
• How to use the induction hypothesis (2 messages, latest: May 31 2023 at 15:29)
• Specifying simprocs (6 messages, latest: May 26 2023 at 18:13)
• Un-indexed sum of finite set of numbers (6 messages, latest: May 26 2023 at 10:24)
• Metric spaces in Isabelle (2 messages, latest: May 25 2023 at 13:33)
• How to define the range lemma like star in Isabelle entry (15 messages, latest: May 23 2023 at 14:37)
• Why does simp fail? (6 messages, latest: May 22 2023 at 02:51)
• Transfer of integrability when adding constant to function (3 messages, latest: May 21 2023 at 10:37)
• Is this tutorial up to date? (3 messages, latest: May 16 2023 at 04:58)
• jEdit notification bell on control characters (1 message, latest: May 11 2023 at 09:57)
• Mechanisms for blocking "nonsensical" statements (8 messages, latest: May 10 2023 at 18:40)
• Vscode Isabelle 2022 (2 messages, latest: May 10 2023 at 16:24)
• Locale with type parameter (2 messages, latest: May 08 2023 at 08:48)
• Isabelle Built-In Theories (3 messages, latest: May 08 2023 at 02:41)
• Find definition of instance (1 message, latest: May 07 2023 at 15:30)
• Reusing set_contains syntax (7 messages, latest: May 06 2023 at 22:25)
• Easy way of expressing term size (4 messages, latest: May 06 2023 at 19:47)
• Qed hangs indefinitely (2 messages, latest: May 06 2023 at 18:43)
• Reordering summations (1 message, latest: May 06 2023 at 13:29)
• Isar proof by 3 disjunctive cases (12 messages, latest: May 06 2023 at 09:13)
• Can I use a custom qualifier name? (3 messages, latest: May 05 2023 at 14:12)
• Integration (9 messages, latest: May 04 2023 at 12:02)
• Haskell like pattern matching "@" operator (5 messages, latest: May 02 2023 at 06:36)
• Focusing the simplifier (21 messages, latest: May 01 2023 at 13:37)
• Term rewrite from outside isabelle (11 messages, latest: Apr 28 2023 at 14:06)
• Remove a type class instance? (1 message, latest: Apr 28 2023 at 02:43)
• ZFC+HOL (4 messages, latest: Apr 27 2023 at 13:30)
• Proof automation questions (3 messages, latest: Apr 25 2023 at 13:06)
• Adding sort constraint to sublocales (1 message, latest: Apr 25 2023 at 11:49)
• Rotation premises of a specific subgoal (4 messages, latest: Apr 22 2023 at 18:22)
• Isabelle in vscode (8 messages, latest: Apr 21 2023 at 21:31)
• Extracting Lemmas and Definitions from Isabelle Proofs (5 messages, latest: Apr 20 2023 at 18:38)
• Defining a function between function types (7 messages, latest: Apr 20 2023 at 08:41)
• Record update syntax (2 messages, latest: Apr 20 2023 at 07:56)
• Isabelle LaTeX documents (6 messages, latest: Apr 18 2023 at 15:29)
• Unprovable termination goal using Monad (2 messages, latest: Apr 17 2023 at 19:42)
• simp and schematics (2 messages, latest: Apr 17 2023 at 15:21)
• Records (2 messages, latest: Apr 14 2023 at 06:31)
• Potentially infinite lists (2 messages, latest: Apr 13 2023 at 15:41)
• How to apply inequality rules in one step (14 messages, latest: Apr 10 2023 at 13:58)
• exception CONTEXT (4 messages, latest: Apr 07 2023 at 08:04)
• Method to instantiate schematic variables in a goal (6 messages, latest: Apr 05 2023 at 10:25)
• Why are modules also rings in the HOL-Algebra library? (6 messages, latest: Mar 29 2023 at 10:12)
• Using keyword using (6 messages, latest: Mar 29 2023 at 06:29)
• Make sledgehammer not use simp (9 messages, latest: Mar 29 2023 at 05:45)
• Finding theorems (2 messages, latest: Mar 27 2023 at 16:05)
• Isabelle/HOL language (2 messages, latest: Mar 26 2023 at 15:49)
• Elimination rule (5 messages, latest: Mar 22 2023 at 08:08)
• Asserting element-wise equality (4 messages, latest: Mar 20 2023 at 16:23)
• Changing variable not being inducted on (3 messages, latest: Mar 15 2023 at 19:31)
• `no_notation` causes major slowdown (2 messages, latest: Mar 07 2023 at 12:42)
• Syntax translations involving locale definitions (1 message, latest: Mar 07 2023 at 10:37)
• Bundle locale notation (5 messages, latest: Mar 07 2023 at 09:57)
• Proof terms in Isabelle (6 messages, latest: Mar 07 2023 at 06:25)
• labelled transition system (6 messages, latest: Mar 03 2023 at 04:31)
• How to define an auxiliary to help prove such a lemma (1 message, latest: Mar 02 2023 at 10:20)
• a lemma prove (1 message, latest: Mar 01 2023 at 09:44)
• Can I customize the generated inference rule? (2 messages, latest: Feb 28 2023 at 14:39)
• Use an equivalence relation to insantiate a class (8 messages, latest: Feb 27 2023 at 16:01)
• Equivalence relation and the simplifier (1 message, latest: Feb 24 2023 at 16:16)
• Don't split implications in `safe` (4 messages, latest: Feb 23 2023 at 19:45)
• Properties after recursive function (9 messages, latest: Feb 23 2023 at 14:28)
• Schematics with multiple constraints (4 messages, latest: Feb 23 2023 at 13:13)
• Ignoring subgoals with too many schematics (3 messages, latest: Feb 21 2023 at 15:18)
• Detect duplicate assumptions (1 message, latest: Feb 18 2023 at 14:01)
• Non-ambiguous syntax for typing (2 messages, latest: Feb 17 2023 at 16:15)
• No proof state in vscode (41 messages, latest: Feb 17 2023 at 13:28)
• Debug infinite loop in simplifier (1 message, latest: Feb 17 2023 at 12:29)
• Folding subgoals (1 message, latest: Feb 17 2023 at 06:49)
• Finite subset lattice "induction" (3 messages, latest: Feb 16 2023 at 07:59)
• Reading the simp_trace (5 messages, latest: Feb 09 2023 at 05:45)
• Code comments (5 messages, latest: Feb 08 2023 at 21:16)
• How can I simplify the following lemmas? (6 messages, latest: Feb 03 2023 at 19:24)
• Is there a particular syntax for Maps of a single element? (6 messages, latest: Feb 01 2023 at 22:06)
• How can I case with integers with a custom split number? (10 messages, latest: Jan 26 2023 at 10:18)
• Problem with pattern match and the simplifier. (9 messages, latest: Jan 25 2023 at 15:17)
• Can I simplify a single Let definition? (4 messages, latest: Jan 25 2023 at 13:36)
• Remember failed tactic invocations (1 message, latest: Jan 20 2023 at 17:50)
• Postpone Goals (3 messages, latest: Jan 16 2023 at 15:39)
• equal summands ==> equal sums (10 messages, latest: Jan 15 2023 at 18:23)
• Lambda expressions (1 message, latest: Jan 12 2023 at 19:10)
• trouble with primcorecursive definition (destructor view)) (6 messages, latest: Jan 10 2023 at 15:14)
• `simp add` fails while `simp only` succeeds -- how? (8 messages, latest: Jan 07 2023 at 19:06)
• Failed to apply `by assumption` debug (7 messages, latest: Jan 05 2023 at 01:54)
• How to count lines of code for Isabelle theories (6 messages, latest: Jan 04 2023 at 17:09)
• Unfolding of let bindings (3 messages, latest: Jan 03 2023 at 21:09)
• Duplicate fact declaration during locale instantiation (5 messages, latest: Jan 02 2023 at 06:55)
• Error Option when closing subgoal with done (3 messages, latest: Dec 20 2022 at 16:03)
• ✔ Rewrite term using a proven "p ==> q" theorem? (9 messages, latest: Dec 20 2022 at 02:19)
• ✔ How to break down these conjuncts directly? (4 messages, latest: Dec 20 2022 at 02:04)
• Showing Max S is in S (4 messages, latest: Dec 19 2022 at 15:34)
• How to break down these conjuncts directly? (6 messages, latest: Dec 19 2022 at 09:09)
• Rewrite term using a proven "p ==> q" theorem? (2 messages, latest: Dec 19 2022 at 06:10)
• Shorthand syntax for constructors (2 messages, latest: Dec 16 2022 at 23:20)
• ✔ Shorthand for current subgoal? (7 messages, latest: Dec 16 2022 at 21:28)
• ✔ Apply iff theorem in one direction? (7 messages, latest: Dec 16 2022 at 21:25)
• Apply iff theorem in one direction? (3 messages, latest: Dec 15 2022 at 08:24)
• Shorthand for current subgoal? (1 message, latest: Dec 15 2022 at 06:01)
• Catalogue in vscode (15 messages, latest: Dec 14 2022 at 13:29)
• ✔ Why not possible to concluce n = 0 here? (2 messages, latest: Dec 13 2022 at 20:48)
• Why not possible to concluce n = 0 here? (2 messages, latest: Dec 13 2022 at 20:00)
• Type synonyms in locales (1 message, latest: Dec 11 2022 at 13:45)
• ✔ How to work with function defs that have lets in proofs (2 messages, latest: Dec 11 2022 at 00:29)
• syntax for Brackets (3 messages, latest: Dec 09 2022 at 18:54)
• Isabelle AFP components (4 messages, latest: Dec 09 2022 at 12:13)
• Parametric polymorphism in locales (13 messages, latest: Dec 07 2022 at 10:00)
• Source code of documentation (3 messages, latest: Dec 06 2022 at 13:02)
• Giving a datatype an "equal" property (12 messages, latest: Dec 05 2022 at 19:13)
• Controlling visibility of theory content (7 messages, latest: Dec 05 2022 at 17:57)
• vscode on Windows (3 messages, latest: Dec 03 2022 at 23:45)
• ✔ No code equation for pairs (4 messages, latest: Dec 01 2022 at 21:30)
• No code equation for pairs (2 messages, latest: Dec 01 2022 at 18:50)
• How to work with function defs that have lets in proofs (2 messages, latest: Dec 01 2022 at 09:47)
• Landau with arity > 1 (4 messages, latest: Nov 30 2022 at 22:20)
• ✔ contribute to isabelle (4 messages, latest: Nov 21 2022 at 05:47)
• Instantiation with multiple type params (5 messages, latest: Nov 17 2022 at 13:34)
• ✔ Typedecl (and Locales) (2 messages, latest: Nov 16 2022 at 23:42)
• Typedecl (and Locales) (6 messages, latest: Nov 16 2022 at 21:06)
• ✔ Set behaviour (4 messages, latest: Nov 14 2022 at 19:43)
• Underdefined vs undefined (15 messages, latest: Nov 14 2022 at 12:04)
• ✔ Distributivity (4 messages, latest: Nov 14 2022 at 10:44)
• building a document (5 messages, latest: Nov 08 2022 at 14:30)
• ✔ Have isabelle code in monospace font in pdf output (2 messages, latest: Nov 07 2022 at 10:16)
• Have isabelle code in monospace font in pdf output (5 messages, latest: Nov 06 2022 at 22:37)
• ✔ Multiple proofs found by cvc4 with sledgehammer (6 messages, latest: Nov 06 2022 at 13:30)
• ✔ jedit not replacing symbols (2 messages, latest: Nov 04 2022 at 11:56)
• jedit not replacing symbols (4 messages, latest: Nov 04 2022 at 10:49)
• ✔ Isabelle vscode in Windows (1 message, latest: Nov 01 2022 at 08:04)
• Purple highlight in the proof (4 messages, latest: Oct 31 2022 at 01:25)
• Isabelle vscode in Windows (3 messages, latest: Oct 30 2022 at 22:27)
• Force Eq instance export (16 messages, latest: Oct 28 2022 at 16:42)
• ✔ Attach restriction to type (1 message, latest: Oct 27 2022 at 15:11)
• Attach restriction to type (5 messages, latest: Oct 26 2022 at 18:21)
• Isabelle vscode in macOS (8 messages, latest: Oct 24 2022 at 04:48)
• ✔ to_nat (from_nat x) = x (3 messages, latest: Oct 21 2022 at 17:18)
• to_nat (from_nat x) = x (4 messages, latest: Oct 21 2022 at 16:39)
• ✔ Is there a shorter way for this? (1 message, latest: Oct 19 2022 at 18:46)
• Is there a shorter way for this? (4 messages, latest: Oct 19 2022 at 18:41)
• ✔ Prove ∃x::A. P x ⟹ ∃x::'a P x (3 messages, latest: Oct 17 2022 at 10:56)
• ✔ Remove ∃x if x has only one possible value (1 message, latest: Oct 15 2022 at 10:55)
• Remove ∃x if x has only one possible value (3 messages, latest: Oct 14 2022 at 15:58)
• Sledgehammer finding something that doesn't seem to terminat (11 messages, latest: Oct 14 2022 at 11:12)
• ✔ proof that countable is linorder (2 messages, latest: Oct 13 2022 at 07:39)
• Proof correctness materials (8 messages, latest: Oct 12 2022 at 18:29)
• proof that countable is linorder (6 messages, latest: Oct 12 2022 at 15:48)
• ✔ partition_on (10 messages, latest: Oct 09 2022 at 21:22)
• partition_on (9 messages, latest: Oct 03 2022 at 18:28)
• ✔ apply case_tac to ∀x. (2 messages, latest: Oct 03 2022 at 10:47)
• apply case_tac to ∀x. (4 messages, latest: Oct 01 2022 at 13:31)
• ✔ Isar re-use facts and`next` (2 messages, latest: Sep 30 2022 at 17:50)
• Isar re-use facts and`next` (2 messages, latest: Sep 30 2022 at 17:00)
• Use of Not in definition (9 messages, latest: Sep 29 2022 at 10:01)
• Obtain set of all members of datatype (6 messages, latest: Sep 29 2022 at 09:45)
• ✔ Controlling OCaml code export (1 message, latest: Sep 17 2022 at 20:30)
• Controlling OCaml code export (4 messages, latest: Sep 17 2022 at 01:58)
• why the following eisbach method definition fail to parse? (6 messages, latest: Sep 16 2022 at 18:04)
• Exporting "nat" to OCaml (4 messages, latest: Sep 15 2022 at 02:31)
• Interpret types as lattices (11 messages, latest: Sep 14 2022 at 16:18)
• ✔ Trying to prove a complete induction (2 messages, latest: Sep 14 2022 at 15:53)
• Trying to prove a complete induction (6 messages, latest: Sep 14 2022 at 13:36)
• ✔ Simple proof for inductive definition (7 messages, latest: Sep 14 2022 at 10:59)
• ✔ Exporting "nat" to OCaml (2 messages, latest: Sep 13 2022 at 21:15)
• limit number of rewrites in simplifier (4 messages, latest: Sep 10 2022 at 03:25)
• ZFC (80 messages, latest: Sep 09 2022 at 21:31)
• ✔ Failure to apply induction on a theorem (11 messages, latest: Sep 05 2022 at 18:03)
• ✔ qed succeeds in Isar proof with error (2 messages, latest: Sep 05 2022 at 15:28)
• qed succeeds in Isar proof with error (4 messages, latest: Sep 05 2022 at 15:22)
• TAPL proof 3.2.5 help (4 messages, latest: Sep 04 2022 at 20:09)
• Failure to apply induction on a theorem (3 messages, latest: Sep 04 2022 at 14:43)
• commutative monoid solver? (6 messages, latest: Sep 02 2022 at 16:49)
• induction with "obtains" (3 messages, latest: Sep 01 2022 at 00:57)
• Axiom schemas in Isabelle (3 messages, latest: Aug 31 2022 at 14:29)
• Running simple code (5 messages, latest: Aug 31 2022 at 14:21)
• Return element of 'a::finite_lattice (3 messages, latest: Aug 30 2022 at 17:28)
• max nat in list (11 messages, latest: Aug 26 2022 at 16:57)
• Nitpick and exceptions (3 messages, latest: Aug 25 2022 at 22:45)
• Lifting of theorems (2 messages, latest: Aug 25 2022 at 22:43)
• Induction over a generalised type (9 messages, latest: Aug 24 2022 at 07:54)
• keybinds in jEdit (2 messages, latest: Aug 24 2022 at 07:45)
• Accessing sublocale information (4 messages, latest: Aug 22 2022 at 02:41)
• proof structure one-liners (3 messages, latest: Aug 21 2022 at 00:51)
• Proving lemma with definite description (9 messages, latest: Aug 16 2022 at 09:47)
• Error: Naproche-SAD (1 message, latest: Aug 15 2022 at 00:36)
• "Enter MATCH" output (2 messages, latest: Aug 14 2022 at 17:30)
• proving set equality in Isabelle/HOL? (2 messages, latest: Aug 13 2022 at 08:00)
• ✔ Proof involving datatype partially? (1 message, latest: Aug 10 2022 at 12:44)
• Proof involving datatype partially? (2 messages, latest: Aug 10 2022 at 09:39)
• ✔ Interpretation in locale context (1 message, latest: Aug 09 2022 at 11:56)
• Interpretation in locale context (4 messages, latest: Aug 08 2022 at 10:56)
• Putting Isabelle code in Latex (2 messages, latest: Aug 08 2022 at 08:59)
• defining module homomorphisms (4 messages, latest: Aug 08 2022 at 03:21)
• uniqueness proof (9 messages, latest: Aug 01 2022 at 15:21)
• unfolding comp_apply also unfolds unapplied comp (2 messages, latest: Jul 31 2022 at 18:24)
• ✔ exception when trying to define function (15 messages, latest: Jul 29 2022 at 12:38)
• exception when trying to define function (16 messages, latest: Jul 29 2022 at 10:33)
• ✔ case of in proof (2 messages, latest: Jul 29 2022 at 09:07)
• case of in proof (2 messages, latest: Jul 28 2022 at 22:46)
• ✔ quickcheck found a counter-example (1 message, latest: Jul 27 2022 at 03:51)
• quickcheck found a counter-example (1 message, latest: Jul 26 2022 at 19:48)
• ✔ Proving a lemma by strong induction (2 messages, latest: Jul 26 2022 at 19:41)
• Document preparation: Repeat definition (1 message, latest: Jul 26 2022 at 15:54)
• ✔ Failing to solve existential goal but metis can (3 messages, latest: Jul 26 2022 at 14:14)
• Failing to solve existential goal but metis can (1 message, latest: Jul 26 2022 at 13:31)
• cases and schematic variables (5 messages, latest: Jul 26 2022 at 12:29)
• Document preparation - automatic build (2 messages, latest: Jul 24 2022 at 10:15)
• Proving a lemma by strong induction (10 messages, latest: Jul 23 2022 at 14:44)
• How do I include external dependencies in exported Haskell? (1 message, latest: Jul 23 2022 at 14:23)
• using "of" (7 messages, latest: Jul 22 2022 at 04:56)
• Ill typed instantiation (3 messages, latest: Jul 22 2022 at 04:52)
• ✔ Strong induction in Isabelle (5 messages, latest: Jul 21 2022 at 12:23)
• ✔ Induction rule error (8 messages, latest: Jul 21 2022 at 12:23)
• ✔ What's wrong with ths statement? (2 messages, latest: Jul 21 2022 at 11:53)
• Code Style Guide? (9 messages, latest: Jul 21 2022 at 05:00)
• jedit issue (7 messages, latest: Jul 19 2022 at 19:13)
• isabelle document (1 message, latest: Jul 19 2022 at 09:03)
• ✔ Proof by induction (4 messages, latest: Jul 18 2022 at 17:11)
• minimal (12 messages, latest: Jul 18 2022 at 15:11)
• How do I approach this proof? (1 message, latest: Jul 18 2022 at 15:08)
• Trichotomy (3 messages, latest: Jul 15 2022 at 20:15)
• Order of arguments in mixfix (1 message, latest: Jul 15 2022 at 10:05)
• Manual proof using <fname>.cases <fname.elims> (8 messages, latest: Jul 07 2022 at 17:01)
• Sledgehammer finds proof metis times out (2 messages, latest: Jul 03 2022 at 16:14)
• Definite Descriptions (11 messages, latest: Jul 02 2022 at 13:34)
• check whether subgoal changed independent of premise order (2 messages, latest: Jul 01 2022 at 11:32)
• ✔ Use type in class declaration (16 messages, latest: Jul 01 2022 at 10:49)
• Proving subgoals with assumptions in other context (1 message, latest: Jul 01 2022 at 10:31)
• How to write this set notation (3 messages, latest: Jun 27 2022 at 22:23)
• ✔ Bad component catalog file error (12 messages, latest: Jun 27 2022 at 17:55)
• ✔ Installation problem with the main plugin (10 messages, latest: Jun 22 2022 at 23:58)
• ✔ prove a formulae on a finite set (7 messages, latest: Jun 19 2022 at 15:38)
• ✔ Real uniform distribution (19 messages, latest: Jun 12 2022 at 20:45)
• ✔ simp add vs using (12 messages, latest: Jun 07 2022 at 19:52)
• Typdefs and code (3 messages, latest: Jun 06 2022 at 03:19)
• setup_lifting and relators (5 messages, latest: May 27 2022 at 14:35)
• Tricks for arithmetic (69 messages, latest: May 19 2022 at 14:14)
• Document about Isar Implementation (2 messages, latest: May 19 2022 at 06:55)
• Tracing the classical reasoner (1 message, latest: May 17 2022 at 06:29)
• ✔ Debug metis (3 messages, latest: May 13 2022 at 08:36)
• ✔ changing ml memory limit (4 messages, latest: May 12 2022 at 10:31)
• Mirabelle/Sledgehammer (3 messages, latest: May 11 2022 at 14:59)
• stream events (3 messages, latest: May 06 2022 at 07:15)
• ✔ Simplifier problem (6 messages, latest: May 05 2022 at 17:37)
• Why natural deduction? (1 message, latest: May 02 2022 at 17:13)
• compare id (1 message, latest: Apr 29 2022 at 14:26)
• theory error (2 messages, latest: Apr 25 2022 at 08:25)
• ✔ Record accessor subscript (3 messages, latest: Apr 23 2022 at 16:49)
• ✔ Concrete Semantics ex 2.3 (3 messages, latest: Apr 23 2022 at 13:25)
• ✔ How can the theory name be omitted? (3 messages, latest: Apr 23 2022 at 09:20)
• ✔ "no type arity" in error message (7 messages, latest: Apr 21 2022 at 16:14)
• Isabelle/Jedit can not startup on win10 (1 message, latest: Apr 21 2022 at 12:20)
• prove function fusion (2 messages, latest: Apr 16 2022 at 03:04)
• ✔ Bad theory import "Draft.*" (8 messages, latest: Apr 15 2022 at 18:48)
• good cheat sheet for beginners (8 messages, latest: Apr 11 2022 at 14:22)
• how to start with Isabelle from scratch? (2 messages, latest: Apr 09 2022 at 10:57)
• homomorphism locales in std lib (5 messages, latest: Apr 07 2022 at 11:33)
• Simple proof using Decision_Procs/Approximation (23 messages, latest: Apr 06 2022 at 06:49)
• ✔ jEdit: Dark Theme (8 messages, latest: Apr 05 2022 at 10:53)
• ✔ locale align/fix type variables. (14 messages, latest: Mar 16 2022 at 18:50)
• IMP Hoare logic (6 messages, latest: Mar 10 2022 at 08:39)
• Name collisions between records (2 messages, latest: Mar 08 2022 at 08:58)
• enumerate all chars and prove exhaustiveness (12 messages, latest: Mar 01 2022 at 18:54)
• ✔ list comprehension (8 messages, latest: Mar 01 2022 at 17:50)
• ✔ Number literals and explicit type annotations (7 messages, latest: Feb 18 2022 at 20:48)
• ✔ Polymorphic HOL vs System F (10 messages, latest: Feb 18 2022 at 15:53)
• tracing inductive definitions (3 messages, latest: Feb 12 2022 at 18:54)
• ✔ built-in functions to convert int to char? (6 messages, latest: Feb 10 2022 at 08:14)
• How to toggle checking mode in a jedit view (3 messages, latest: Feb 08 2022 at 13:49)
• How to access definitions generated by Inductive package (8 messages, latest: Feb 07 2022 at 21:17)
• Splitting conjunction (5 messages, latest: Feb 07 2022 at 16:09)
• ✔ Obvious subgoal failed sledgehammer (5 messages, latest: Feb 07 2022 at 08:03)
• ✔ Understanding syntax definitions (3 messages, latest: Feb 05 2022 at 03:40)
• How to approach this formalization (3 messages, latest: Feb 04 2022 at 06:35)
• ✔ HOL Library Recompiles every time (15 messages, latest: Feb 02 2022 at 17:44)
• ✔ How to print proof terms (3 messages, latest: Jan 26 2022 at 19:35)
• Emacs Set Mark Error (1 message, latest: Jan 24 2022 at 13:04)
• ✔ "Extracting" field names from records (7 messages, latest: Jan 24 2022 at 06:42)
• disable eta-contraction in printing (4 messages, latest: Jan 24 2022 at 06:05)
• Sledgehammer in ZF (8 messages, latest: Jan 11 2022 at 22:58)
• ✔ Changing Options in Isabelle2021-1 (6 messages, latest: Jan 06 2022 at 09:48)
• ✔ Proving lemma about IMP codes (3 messages, latest: Dec 20 2021 at 15:21)
• code generation (3 messages, latest: Dec 16 2021 at 15:58)
• ✔ solve by assumption (3 messages, latest: Dec 14 2021 at 18:26)
• ✔ div2 induction example (3 messages, latest: Dec 14 2021 at 16:55)
• ✔ debug unification (7 messages, latest: Dec 08 2021 at 14:04)
• ✔ How to inspect the domain and range of a function? (6 messages, latest: Dec 08 2021 at 12:46)
• splitting cases in goal with schematic variables (3 messages, latest: Dec 08 2021 at 11:25)
• ✔ Dealing with trivial arithmetic (9 messages, latest: Dec 08 2021 at 11:21)
• Associativity Map Composition (1 message, latest: Dec 04 2021 at 07:58)
• ✔ How to prevent splitting of pair in universial quantifi... (6 messages, latest: Dec 01 2021 at 06:51)
• ✔ Defining class with at least two members satisfying pro... (3 messages, latest: Nov 28 2021 at 12:55)
• Can I use a locale to define a language? (2 messages, latest: Nov 28 2021 at 12:39)
• ✔ Proving symmetry of serialization of nats (21 messages, latest: Nov 27 2021 at 22:34)
• How to "clean up" assumptions for related free variables? (1 message, latest: Nov 27 2021 at 20:13)
• ✔ Simplification rules not applying to records (6 messages, latest: Nov 25 2021 at 15:08)
• ✔ how to import "HOL-Lattice.Orders" (15 messages, latest: Nov 24 2021 at 17:12)
• ✔ alternative to Scratch.thy? (5 messages, latest: Nov 23 2021 at 13:01)
• ✔ Where to put assumptions in Isar proof (6 messages, latest: Nov 21 2021 at 13:34)
• ✔ option predicate (5 messages, latest: Nov 16 2021 at 18:07)
• ✔ Name of the Language used in .thy files (11 messages, latest: Nov 15 2021 at 01:39)
• Specialize locales incl. defines (4 messages, latest: Nov 14 2021 at 17:43)
• ✔ Proving a mutex (10 messages, latest: Nov 14 2021 at 13:31)
• ✔ Disable unfolding of let expressions (7 messages, latest: Nov 09 2021 at 20:51)
• ✔ Double quotes in pdf output (8 messages, latest: Nov 07 2021 at 18:04)
• ✔ jEdit format entire theory (4 messages, latest: Nov 07 2021 at 13:13)
• What, Why and How!!! (4 messages, latest: Nov 04 2021 at 04:45)
• ✔ adding development version afp components breaks Isabelle (8 messages, latest: Oct 18 2021 at 14:56)
• Installing Isabelle (11 messages, latest: Oct 13 2021 at 08:02)
• Can you convert from prop back to bool? (6 messages, latest: Sep 30 2021 at 23:04)
• termination adding assumption (1 message, latest: Sep 27 2021 at 14:21)
• Documentation unify_trace_failure (1 message, latest: Sep 26 2021 at 09:25)
• ✔ using "term t" prove "term t" not working (4 messages, latest: Sep 21 2021 at 08:57)
• ✔ Recursive datatype sets bnf (4 messages, latest: Sep 20 2021 at 16:30)
• ✔ Infix syntax (4 messages, latest: Sep 19 2021 at 19:20)
• Product in simple type theory (7 messages, latest: Sep 14 2021 at 18:37)
• Command "imports" does not end (3 messages, latest: Sep 14 2021 at 13:01)
• ✔ locale context & assumptions\goals (5 messages, latest: Sep 13 2021 at 15:18)
• ✔ rule_tac vs [where ..] (5 messages, latest: Sep 06 2021 at 05:14)
• ✔ Failed to apply proof method (3 messages, latest: Sep 04 2021 at 16:51)
• ✔ proving the correctness of an algorithm (4 messages, latest: Aug 30 2021 at 18:24)
• ✔ symmetric rule in inductively defined predicates (28 messages, latest: Aug 20 2021 at 15:59)
• ✔ the meaning of "no solution" for a function equation (12 messages, latest: Aug 20 2021 at 15:59)
• ✔ proof pattern for set equality (9 messages, latest: Aug 18 2021 at 20:00)
• ✔ Coinductive/inductive reasoning (7 messages, latest: Aug 18 2021 at 19:19)
• ✔ Instanciation of schematic variables in ML (6 messages, latest: Aug 18 2021 at 11:02)
• ✔ Additional type variable (2 messages, latest: Aug 16 2021 at 19:14)
• Using the ISA AFP (10 messages, latest: Aug 13 2021 at 15:01)
• Traits -> Isabelle (3 messages, latest: Aug 13 2021 at 10:26)
• ✔ Prove lemma "¬¬ (A ∨ ¬A)" by natural deduction (7 messages, latest: Aug 13 2021 at 07:51)
• Emacs Set Mark (1 message, latest: Aug 01 2021 at 05:37)
• Delete i-th premise of subgoal (2 messages, latest: Jul 27 2021 at 21:36)
• evaluation value\theorem (3 messages, latest: Jul 21 2021 at 19:07)
• "'a itself" documentation (14 messages, latest: Jul 21 2021 at 10:09)
• fresh names (39 messages, latest: Jul 18 2021 at 18:29)
• Wellorder instance of char (7 messages, latest: Jul 18 2021 at 17:41)
• convert map to list (5 messages, latest: Jul 18 2021 at 14:46)
• Find instances (6 messages, latest: Jul 16 2021 at 20:09)
• Disable simp for IH (10 messages, latest: Jul 13 2021 at 23:38)
• Dependecy graphs (2 messages, latest: Jul 11 2021 at 16:34)
• Convert a char to nat (3 messages, latest: Jul 09 2021 at 08:20)
• Undefined control sequence (4 messages, latest: Jul 06 2021 at 16:56)
• Collect optional values (1 message, latest: Jul 06 2021 at 09:58)
• good HTML but empty pdf (4 messages, latest: Jul 06 2021 at 00:39)
• splitWith missing in List.thy ? (6 messages, latest: Jul 05 2021 at 19:57)
• Abstract_topology (5 messages, latest: Jul 01 2021 at 15:47)
• Isabelle loosing typecheck memory (14 messages, latest: Jul 01 2021 at 11:53)
• closure_of (5 messages, latest: Jun 30 2021 at 15:09)
• Black proof instead of red (4 messages, latest: Jun 30 2021 at 08:43)
• Sledgehammer timeout option (4 messages, latest: Jun 29 2021 at 15:07)
• Local homeomorphism (18 messages, latest: Jun 29 2021 at 11:16)
• Threaded view (12 messages, latest: Jun 28 2021 at 16:28)
• binary numbers (10 messages, latest: Jun 26 2021 at 09:27)
• learning resources (22 messages, latest: Jun 25 2021 at 18:06)
• Topology with the axiom of choice (1 message, latest: Jun 24 2021 at 19:57)
• Inverse of bijective function (21 messages, latest: Jun 24 2021 at 19:14)
• very new to isabelle, can't open WasmCert (13 messages, latest: Jun 24 2021 at 17:17)
• Unfinished termination proof allows to finish proof (10 messages, latest: Jun 23 2021 at 13:43)
• Isomorphism on (2 messages, latest: Jun 22 2021 at 20:14)
• ((A ==> B) & A) ==> B? (18 messages, latest: Jun 21 2021 at 16:25)
• Changing type classes in locales (22 messages, latest: Jun 21 2021 at 15:38)
• Fix 'a with typeclass (15 messages, latest: Jun 21 2021 at 13:48)
• theory Aux (1 message, latest: Jun 20 2021 at 08:07)
• real_vector.subspace (20 messages, latest: Jun 17 2021 at 18:23)
• Why Pure.conjunctionI is an "ill-formed introduction rule"? (9 messages, latest: Jun 15 2021 at 08:20)
• How to get all elimination rules? (2 messages, latest: Jun 15 2021 at 04:42)
• Sum of functions (19 messages, latest: Jun 11 2021 at 13:31)
• pending (15 messages, latest: Jun 09 2021 at 14:09)
• THE (5 messages, latest: Jun 09 2021 at 04:53)
• Could a translation rule be disabled by an option? (1 message, latest: Jun 08 2021 at 11:14)
• Inductive proof over accumulator (22 messages, latest: Jun 07 2021 at 13:03)
• Pattern Aliases (5 messages, latest: Jun 04 2021 at 19:57)
• manual method for forall-elimination (22 messages, latest: Jun 04 2021 at 11:27)
• reset (3 messages, latest: Jun 03 2021 at 13:07)
• extend_nat (3 messages, latest: Jun 02 2021 at 13:16)
• conditional (2 messages, latest: Jun 02 2021 at 02:41)
• Typeclass constraint on implicit 'a (2 messages, latest: May 30 2021 at 19:42)
• Forward declaration (4 messages, latest: May 28 2021 at 11:02)
• instantiation (7 messages, latest: May 27 2021 at 15:40)
• Isabelle Listings in LaTeX (4 messages, latest: May 27 2021 at 13:35)
• afp (58 messages, latest: May 26 2021 at 11:37)
• Partial function as parameter (3 messages, latest: May 25 2021 at 11:32)
• Folding over a Map (22 messages, latest: May 23 2021 at 18:19)
• chernoff (11 messages, latest: May 21 2021 at 16:34)
• HOL library organization (10 messages, latest: May 17 2021 at 12:58)
• Predicate get element from set (4 messages, latest: May 13 2021 at 17:21)
• Abs_filter (9 messages, latest: May 12 2021 at 18:30)
• Explicit syntax: multi-character \<sub> and \<sup> ? (8 messages, latest: May 10 2021 at 09:47)
• 'a option vs underspecified (7 messages, latest: May 08 2021 at 20:01)
• Type overloading not working (33 messages, latest: May 07 2021 at 00:02)
• Isabelle in command line (16 messages, latest: May 05 2021 at 18:16)
• shortcut (5 messages, latest: May 05 2021 at 16:25)
• nested lambda (21 messages, latest: May 03 2021 at 19:00)
• Cantor's pairing function (14 messages, latest: May 03 2021 at 14:10)
• First-order logic on graphs (1 message, latest: Apr 29 2021 at 19:06)
• Complexity proofs with logarithm (5 messages, latest: Apr 29 2021 at 09:46)
• Lifting a relation to a quotient (2 messages, latest: Apr 29 2021 at 09:21)
• Strong Induction (2 messages, latest: Apr 28 2021 at 13:43)
• Unbound Schematic Variable (8 messages, latest: Apr 27 2021 at 16:22)
• arithmetic reasoning (6 messages, latest: Apr 27 2021 at 14:34)
• finite_induct over sets (42 messages, latest: Apr 27 2021 at 11:19)
• divide (4 messages, latest: Apr 27 2021 at 04:30)
• Polymorphic recursion (11 messages, latest: Apr 26 2021 at 14:13)
• Generic 'a set set => 'a set (6 messages, latest: Apr 24 2021 at 18:32)
• Sort inference? (4 messages, latest: Apr 23 2021 at 13:22)
• Isabelle2020 (2 messages, latest: Apr 22 2021 at 21:30)
• sqrt (10 messages, latest: Apr 22 2021 at 16:55)
• jEdit style (10 messages, latest: Apr 22 2021 at 11:58)
• locale for vector spaces (5 messages, latest: Apr 22 2021 at 08:51)
• sublocale (15 messages, latest: Apr 21 2021 at 16:05)
• ML documentation (5 messages, latest: Apr 14 2021 at 19:48)
• show (35 messages, latest: Apr 14 2021 at 14:56)
• gcd (2 messages, latest: Apr 13 2021 at 15:17)
• Isabelle takes ~5 mins for a simple function definition (13 messages, latest: Apr 13 2021 at 10:20)
• import quotes (6 messages, latest: Apr 13 2021 at 09:30)
• Removing assumptions in apply style proofs (4 messages, latest: Apr 12 2021 at 11:00)
• Show inductive hyps in state (5 messages, latest: Mar 24 2021 at 17:19)
• Continuous "ML Cleanup" (6 messages, latest: Mar 22 2021 at 08:07)
• Introductory explanation of lifting and transfer (22 messages, latest: Mar 20 2021 at 14:39)
• @{const} antiquotation before definition (2 messages, latest: Mar 19 2021 at 12:26)
• Go-to-definition for fancy syntax (3 messages, latest: Mar 19 2021 at 08:57)
• Difference between = and ≡ (8 messages, latest: Mar 17 2021 at 20:14)
• intro exI is overzealous (6 messages, latest: Mar 12 2021 at 08:35)
• ML memory usage goes up (4 messages, latest: Mar 06 2021 at 11:12)
• Nitpick and Sledgehammer both succesfull (6 messages, latest: Mar 02 2021 at 14:29)
• Numeric type conversion (15 messages, latest: Feb 25 2021 at 23:51)
• Where is Isabelle/LK (1 message, latest: Feb 23 2021 at 21:06)
• relating list indices to appended lists (3 messages, latest: Feb 13 2021 at 00:19)
• short syntax for multiple ∀ (1 message, latest: Feb 12 2021 at 20:26)
• Refer to theorems introduced by sublocale (2 messages, latest: Feb 12 2021 at 10:40)
• machine word (morphisms) (11 messages, latest: Feb 10 2021 at 15:08)
• Debugging heap rebuilds (47 messages, latest: Feb 09 2021 at 11:07)
• substituting into a congruence (2 messages, latest: Feb 07 2021 at 13:29)
• unfold, but just once (4 messages, latest: Feb 06 2021 at 06:22)
• Equivalent locales (22 messages, latest: Feb 05 2021 at 12:44)
• LaTeX cross-references in Isabelle documents (7 messages, latest: Jan 30 2021 at 18:14)
• semiring_modulo for a factorial_semiring + comm_ring (11 messages, latest: Jan 28 2021 at 14:59)
• Pure.cong? (3 messages, latest: Jan 28 2021 at 13:12)
• Doing induction on two variables (2 messages, latest: Jan 27 2021 at 11:22)
• Non-constructor pattern (28 messages, latest: Jan 27 2021 at 11:20)
• Feeding knowledge about functions (28 messages, latest: Jan 26 2021 at 14:56)
• Automation-friendly distinctness constraint (4 messages, latest: Jan 26 2021 at 12:22)
• Termination of a complex recursive function (5 messages, latest: Jan 25 2021 at 12:47)
• split vs cases (7 messages, latest: Jan 22 2021 at 08:57)
• plugins for a faster editing (21 messages, latest: Jan 22 2021 at 08:35)
• Proof method in purple (8 messages, latest: Jan 20 2021 at 11:15)
• something better than auto (7 messages, latest: Jan 20 2021 at 10:24)
• mixed messages (6 messages, latest: Jan 20 2021 at 09:41)
• fun _def or .simps? (12 messages, latest: Jan 20 2021 at 08:52)
• Using bound type variables in a type_synonym (7 messages, latest: Jan 18 2021 at 12:01)
• How to deal with name shadowing? (6 messages, latest: Jan 16 2021 at 23:01)
• Unexpected behaviour of Pattern.matches (8 messages, latest: Jan 12 2021 at 16:49)
• Isar: Fix with restriction (9 messages, latest: Jan 06 2021 at 11:04)
• Limit proof with real power (9 messages, latest: Jan 05 2021 at 15:44)
• Copying theorem output into e-mail (8 messages, latest: Jan 05 2021 at 13:55)
• Building a session document (6 messages, latest: Jan 04 2021 at 10:16)
• Proving lemma with abstract lists (1 message, latest: Dec 28 2020 at 01:00)
• Cardinality of powerset of a multiset (6 messages, latest: Dec 24 2020 at 15:20)
• Numeric literals (2 messages, latest: Dec 22 2020 at 08:53)
• disjoint union of sets (3 messages, latest: Dec 13 2020 at 15:33)
• Import Executable_Set (34 messages, latest: Dec 01 2020 at 19:41)
• group theory (10 messages, latest: Dec 01 2020 at 18:30)
• lemma cannot prove my formula (9 messages, latest: Nov 23 2020 at 09:54)
• Using LaTeXsugar (3 messages, latest: Nov 20 2020 at 11:50)
• polynomials (17 messages, latest: Nov 20 2020 at 11:49)
• typesetting a former definition (1 message, latest: Nov 13 2020 at 08:40)
• Implicit use of directory (6 messages, latest: Nov 13 2020 at 07:51)
• referring to a definition (11 messages, latest: Nov 11 2020 at 10:09)
• archive of formal proofs (6 messages, latest: Nov 09 2020 at 19:53)
• Defining partial functions (44 messages, latest: Nov 09 2020 at 13:41)
• Using insert on just one subgoal (3 messages, latest: Nov 06 2020 at 13:16)
• Using rule in isar proofs to setup assumptions (5 messages, latest: Nov 05 2020 at 11:25)
• Defining and using set of functions (20 messages, latest: Nov 02 2020 at 14:47)
• Document preparation: bad parent session (5 messages, latest: Oct 29 2020 at 18:39)
• Proof methods for software verification (44 messages, latest: Oct 20 2020 at 09:29)
• Using locales as "namespace"? (14 messages, latest: Oct 14 2020 at 12:06)
• cite antiquotation (2 messages, latest: Sep 17 2020 at 15:00)
• Set.filter vs Set comprehension (4 messages, latest: Sep 03 2020 at 12:16)
• cases of an inductive definition (5 messages, latest: Aug 26 2020 at 07:47)
• Pale blue i (2 messages, latest: Aug 26 2020 at 07:38)
• definition of a constant (5 messages, latest: Aug 25 2020 at 13:44)
• locale syntax (6 messages, latest: Aug 25 2020 at 12:38)
• Automatic reordering of current facts to apply rule (10 messages, latest: Aug 19 2020 at 07:03)
• Certified terms (7 messages, latest: Aug 18 2020 at 14:42)
• Inspecting context (21 messages, latest: Aug 18 2020 at 12:02)
• Locales as modules (2 messages, latest: Aug 13 2020 at 09:09)
• Additional type variable in an extended locale (3 messages, latest: Aug 12 2020 at 07:19)
• type declarations in a locale (5 messages, latest: Aug 10 2020 at 13:06)
• Typesetting math notation (20 messages, latest: Aug 10 2020 at 11:34)
• Finishing a proof (4 messages, latest: Aug 07 2020 at 08:00)
• Assigning to schematic variable (3 messages, latest: Aug 06 2020 at 10:52)
• Using *this* twice (2 messages, latest: Aug 05 2020 at 11:57)
• Tactic that fails with no premises (8 messages, latest: Aug 05 2020 at 11:37)
• Isar for if-then-else (3 messages, latest: Aug 04 2020 at 14:32)
• Referring to a type class (15 messages, latest: Aug 04 2020 at 12:28)
• Ambigous parsing (5 messages, latest: Aug 04 2020 at 12:01)
• Github (13 messages, latest: Jul 25 2020 at 08:19)
• OF: resolving premise that is an implication (14 messages, latest: Jul 21 2020 at 10:39)
• Bad session "<Session_Name>" (5 messages, latest: Jul 13 2020 at 08:43)
• Apply theorem to assumptions (11 messages, latest: Jun 19 2020 at 15:22)
• using and applying rule (28 messages, latest: Jun 19 2020 at 11:40)
• Schematic variables to meta-quantified (4 messages, latest: May 27 2020 at 14:15)
• Locale assumptions (5 messages, latest: May 26 2020 at 19:59)

Last updated: Jul 16 2026 at 21:01 UTC