ML documentation (5 messages, latest: Apr 14 2021 at 19:48)
show (19 messages, latest: Apr 14 2021 at 14:56)
Induction can’t be applied (16 messages, latest: Apr 14 2021 at 12:16)
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)
(no topic) (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)
finite_induct over sets (30 messages, latest: Mar 11 2021 at 17:13)
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)
Installing Isabelle (5 messages, latest: Jan 02 2021 at 17:34)
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)
code generation (2 messages, latest: Oct 12 2020 at 08:44)
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 “
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)
stream events (2 messages, latest: May 12 2020 at 13:44)
Last updated: Apr 16 2021 at 07:00 UTC