Topics:
- ZFC (67 messages, latest: Jul 06 2022 at 06:49)
- 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 (5 messages, latest: Jul 01 2022 at 10:49)
- Proving subgoals with assumptions in other context (1 message, latest: Jul 01 2022 at 10:31)
- Use type in class declaration (11 messages, latest: Jun 30 2022 at 13:39)
- How to write this set notation (3 messages, latest: Jun 27 2022 at 22:23)
- ✔ Bad component catalog file error (2 messages, latest: Jun 27 2022 at 17:55)
- Bad component catalog file error (10 messages, latest: Jun 27 2022 at 09:40)
- ✔ Installation problem with the main plugin (2 messages, latest: Jun 22 2022 at 23:58)
- Installation problem with the main plugin (8 messages, latest: Jun 20 2022 at 12:24)
- ✔ prove a formulae on a finite set (3 messages, latest: Jun 19 2022 at 15:38)
- prove a formulae on a finite set (4 messages, latest: Jun 19 2022 at 13:51)
- ✔ Real uniform distribution (8 messages, latest: Jun 12 2022 at 20:45)
- Real uniform distribution (11 messages, latest: Jun 11 2022 at 17:02)
- ✔ simp add vs using (2 messages, latest: Jun 07 2022 at 19:52)
- simp add vs using (10 messages, latest: Jun 07 2022 at 15:57)
- 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 (1 message, latest: May 13 2022 at 08:36)
- Debug metis (2 messages, latest: May 13 2022 at 08:26)
- ✔ changing ml memory limit (1 message, latest: May 12 2022 at 10:31)
- changing ml memory limit (3 messages, latest: May 12 2022 at 07:37)
- Mirabelle/Sledgehammer (3 messages, latest: May 11 2022 at 14:59)
- stream events (3 messages, latest: May 06 2022 at 07:15)
- ✔ Simplifier problem (1 message, latest: May 05 2022 at 17:37)
- Simplifier problem (5 messages, latest: May 05 2022 at 17:10)
- Malformed global fact: illegal fixed variable (4 messages, latest: May 03 2022 at 09:09)
- 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 (2 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? (1 message, latest: Apr 23 2022 at 09:20)
- How can the theory name be omitted? (2 messages, latest: Apr 23 2022 at 09:07)
- Record accessor subscript (1 message, latest: Apr 22 2022 at 11:43)
- ✔ "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 (7 messages, latest: Apr 05 2022 at 10:53)
- jEdit: Dark Theme (1 message, latest: Apr 04 2022 at 13:33)
- ✔ locale align/fix type variables. (2 messages, latest: Mar 16 2022 at 18:50)
- locale align/fix type variables. (12 messages, latest: Mar 16 2022 at 07:57)
- 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 (2 messages, latest: Mar 01 2022 at 17:50)
- ✔ Number literals and explicit type annotations (2 messages, latest: Feb 18 2022 at 20:48)
- ✔ Polymorphic HOL vs System F (2 messages, latest: Feb 18 2022 at 15:53)
- Number literals and explicit type annotations (5 messages, latest: Feb 18 2022 at 15:49)
- Polymorphic HOL vs System F (8 messages, latest: Feb 14 2022 at 11:54)
- tracing inductive definitions (3 messages, latest: Feb 12 2022 at 18:54)
- list comprehension (6 messages, latest: Feb 11 2022 at 08:37)
- ✔ built-in functions to convert int to char? (2 messages, latest: Feb 10 2022 at 08:14)
- built-in functions to convert int to char? (4 messages, latest: Feb 09 2022 at 18:44)
- 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 (1 message, latest: Feb 07 2022 at 08:03)
- Obvious subgoal failed sledgehammer (4 messages, latest: Feb 06 2022 at 23:11)
- ✔ Understanding syntax definitions (1 message, latest: Feb 05 2022 at 03:40)
- How to approach this formalization (3 messages, latest: Feb 04 2022 at 06:35)
- Understanding syntax definitions (2 messages, latest: Feb 03 2022 at 09:24)
- ✔ HOL Library Recompiles every time (15 messages, latest: Feb 02 2022 at 17:44)
- ✔ How to print proof terms (1 message, latest: Jan 26 2022 at 19:35)
- How to print proof terms (2 messages, latest: Jan 26 2022 at 18:10)
- Emacs Set Mark Error (1 message, latest: Jan 24 2022 at 13:04)
- ✔ "Extracting" field names from records (1 message, latest: Jan 24 2022 at 06:42)
- disable eta-contraction in printing (1 message, latest: Jan 24 2022 at 06:05)
- "Extracting" field names from records (6 messages, latest: Jan 22 2022 at 12:08)
- Sledgehammer in ZF (8 messages, latest: Jan 11 2022 at 22:58)
- ✔ Changing Options in Isabelle2021-1 (4 messages, latest: Jan 06 2022 at 09:48)
- Changing Options in Isabelle2021-1 (2 messages, latest: Jan 04 2022 at 12:15)
- ✔ Proving lemma about IMP codes (1 message, latest: Dec 20 2021 at 15:21)
- code generation (3 messages, latest: Dec 16 2021 at 15:58)
- ✔ solve by assumption (1 message, latest: Dec 14 2021 at 18:26)
- ✔ div2 induction example (1 message, latest: Dec 14 2021 at 16:55)
- solve by assumption (1 message, latest: Dec 14 2021 at 00:56)
- (no topic) (7 messages, latest: Dec 13 2021 at 20:01)
- div2 induction example (2 messages, latest: Dec 13 2021 at 07:35)
- ✔ debug unification (2 messages, latest: Dec 08 2021 at 14:04)
- ✔ How to inspect the domain and range of a function? (1 message, 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 (3 messages, latest: Dec 08 2021 at 11:21)
- debug unification (5 messages, latest: Dec 08 2021 at 11:19)
- How to inspect the domain and range of a function? (5 messages, latest: Dec 06 2021 at 18:41)
- Associativity Map Composition (1 message, latest: Dec 04 2021 at 07:58)
- Dealing with trivial arithmetic (6 messages, latest: Dec 01 2021 at 18:39)
- ✔ 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 property (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 (9 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 (5 messages, latest: Nov 25 2021 at 15:08)
- Simplification rules not applying to records (1 message, latest: Nov 25 2021 at 14:16)
- Proving symmetry of serialization of nats (12 messages, latest: Nov 25 2021 at 10:08)
- ✔ how to import "HOL-Lattice.Orders" (5 messages, latest: Nov 24 2021 at 17:12)
- how to import "HOL-Lattice.Orders" (10 messages, latest: Nov 24 2021 at 08:03)
- ✔ alternative to Scratch.thy? (2 messages, latest: Nov 23 2021 at 13:01)
- alternative to Scratch.thy? (3 messages, latest: Nov 23 2021 at 10:45)
- ✔ Where to put assumptions in Isar proof (1 message, latest: Nov 21 2021 at 13:34)
- Where to put assumptions in Isar proof (5 messages, latest: Nov 21 2021 at 13:09)
- ✔ option predicate (5 messages, latest: Nov 16 2021 at 18:07)
- ✔ Name of the Language used in .thy files (5 messages, latest: Nov 15 2021 at 01:39)
- Specialize locales incl. defines (4 messages, latest: Nov 14 2021 at 17:43)
- ✔ Proving a mutex (1 message, latest: Nov 14 2021 at 13:31)
- Name of the Language used in .thy files (6 messages, latest: Nov 14 2021 at 12:29)
- ✔ Disable unfolding of let expressions (1 message, latest: Nov 09 2021 at 20:51)
- Proving lemma about IMP codes (2 messages, latest: Nov 09 2021 at 14:01)
- Disable unfolding of let expressions (6 messages, latest: Nov 09 2021 at 10:05)
- ✔ Double quotes in pdf output (2 messages, latest: Nov 07 2021 at 18:04)
- Double quotes in pdf output (6 messages, latest: Nov 07 2021 at 14:25)
- ✔ jEdit format entire theory (2 messages, latest: Nov 07 2021 at 13:13)
- jEdit format entire theory (2 messages, latest: Nov 07 2021 at 07:52)
- What, Why and How!!! (4 messages, latest: Nov 04 2021 at 04:45)
- Proving a mutex (9 messages, latest: Oct 28 2021 at 06:27)
- ✔ adding development version afp components breaks Isabelle (1 message, latest: Oct 18 2021 at 14:56)
- adding development version afp components breaks Isabelle (5 messages, latest: Oct 17 2021 at 16:58)
- adding afp as components causes bean shell error (2 messages, latest: Oct 17 2021 at 14:59)
- 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)
- Dcoumentation 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 (2 messages, latest: Sep 20 2021 at 16:30)
- Recursive datatype sets bnf (2 messages, latest: Sep 20 2021 at 16:11)
- ✔ Infix syntax (2 messages, latest: Sep 19 2021 at 19:20)
- Infix syntax (2 messages, latest: Sep 19 2021 at 18:33)
- 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 (1 message, latest: Sep 13 2021 at 15:18)
- locale context & assumptions\goals (4 messages, latest: Sep 06 2021 at 19:28)
- ✔ rule_tac vs [where ..] (3 messages, latest: Sep 06 2021 at 05:14)
- ✔ Failed to apply proof method (1 message, latest: Sep 04 2021 at 16:51)
- Failed to apply proof method (2 messages, latest: Sep 02 2021 at 18:45)
- rule_tac vs [where ..] (2 messages, latest: Sep 02 2021 at 06:35)
- ✔ proving the correctness of an algorithm (2 messages, latest: Aug 30 2021 at 18:24)
- proving the correctness of an algorithm (2 messages, latest: Aug 29 2021 at 14:39)
- ✔ symmetric rule in inductively defined predicates (1 message, latest: Aug 20 2021 at 15:59)
- ✔ the meaning of "no solution" for a function equation (1 message, latest: Aug 20 2021 at 15:59)
- symmetric rule in inductively defined predicates (27 messages, latest: Aug 20 2021 at 15:13)
- the meaning of "no solution" for a function equation (11 messages, latest: Aug 19 2021 at 19:59)
- ✔ proof pattern for set equality (8 messages, latest: Aug 18 2021 at 20:00)
- ✔ Coinductive/inductive reasoning (1 message, latest: Aug 18 2021 at 19:19)
- proof pattern for set equality (1 message, latest: Aug 18 2021 at 19:14)
- ✔ Instanciation of schematic variables in ML (5 messages, latest: Aug 18 2021 at 11:02)
- Instanciation of schematic variables in ML (1 message, latest: Aug 18 2021 at 10:13)
- Coinductive/inductive reasoning (6 messages, latest: Aug 17 2021 at 05:45)
- ✔ 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 (2 messages, latest: Aug 13 2021 at 07:51)
- Prove lemma "¬¬ (A ∨ ¬A)" by natural deduction (5 messages, latest: Aug 12 2021 at 15:48)
- Emacs Set Mark (1 message, latest: Aug 01 2021 at 05:37)
- Delete i-th premise of subgoal (1 message, latest: Jul 27 2021 at 21:36)
- Delete i-th premise in subgoal (1 message, latest: Jul 27 2021 at 14:13)
- 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)
- disable eta-conversion in term parsing (3 messages, latest: Jul 12 2021 at 05:15)
- 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)
- minimal (3 messages, latest: Jun 02 2021 at 14:02)
- 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)
- 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 07 2022 at 04:05 UTC