Zulip Chat Archive

Stream: Beginner Questions

Topics:

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)
Code generation from locale interpretations within locale (1 message, latest: Aug 28 2023 at 07:51)
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: Nov 13 2025 at 04:27 UTC