Newsgroup:
fa.isabelle
Add New Display Options
20
replies
[isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by Kunčar/Popescu
started 2016-08-18 20:19:19 UTC
2016-08-24 10:41:39 UTC
Jeremy Dawson
13
replies
[isabelle] The presentation of Goedel's First Incompleteness Theorem by Lawrence C. Paulson (and others)
started 2015-12-22 10:58:29 UTC
2016-08-13 15:38:36 UTC
Ken Kubota
1
reply
[isabelle] Question about numerals
started 2016-08-13 15:38:30 UTC
2016-08-13 15:38:34 UTC
Lawrence Paulson
1
reply
[isabelle] Issue with smt and linear arithmetic
started 2016-08-13 07:56:18 UTC
2016-08-13 15:38:32 UTC
Lawrence Paulson
1
reply
[isabelle] Eisbach: fold and named_theorems
started 2016-08-11 07:06:33 UTC
2016-08-11 07:14:58 UTC
Andreas Lochbihler
10
replies
[isabelle] qed and done take long for large goal states
started 2016-07-07 08:09:17 UTC
2016-08-10 14:08:39 UTC
Makarius
2
replies
[isabelle] Proving something is an instance of a locale
started 2016-08-01 09:47:17 UTC
2016-08-10 07:16:45 UTC
Lars Hupel
2
replies
[isabelle] difficulties with polymorphic record extension
started 2016-07-27 13:44:27 UTC
2016-08-08 19:52:04 UTC
Elsa L. Gunter
1
reply
[isabelle] type unification failed using an old lemma?
started 2016-08-05 14:29:49 UTC
2016-08-05 15:47:08 UTC
Mark Wassell
7
replies
[isabelle] Proposal: An update to Multiset theory
started 2016-07-26 12:56:14 UTC
2016-08-05 15:02:20 UTC
Bertram Felgenhauer via Cl-isabelle-users
2
replies
[isabelle] Nominal2 Errors in simple datatype declarations
started 2016-08-04 09:01:25 UTC
2016-08-05 09:40:09 UTC
Edward Pierzchalski
2
replies
[isabelle] Customise the Haskell code generator?
started 2016-08-03 11:05:38 UTC
2016-08-05 08:01:30 UTC
Lars Hupel
3
replies
[isabelle] [noob] Classification functions as part of type definition?
started 2016-08-02 16:05:27 UTC
2016-08-02 21:14:05 UTC
Lars Hupel
5
replies
[isabelle] Continuing with a proof after a failed 'done'
started 2016-08-02 14:41:21 UTC
2016-08-02 15:26:52 UTC
Makarius
3
replies
[isabelle] \<^descr>
started 2016-08-02 09:45:32 UTC
2016-08-02 13:29:20 UTC
Makarius
4
replies
[isabelle] Usability of lift_bnf/copy_bnf
started 2016-08-01 07:31:10 UTC
2016-08-02 06:34:20 UTC
Lars Hupel
10
replies
[isabelle] Plugin error with Isabelle-2016
started 2016-07-25 07:42:56 UTC
2016-08-01 12:17:09 UTC
Makarius
1
reply
[isabelle] Report from our Isabelle course
started 2016-07-20 11:43:54 UTC
2016-08-01 08:02:20 UTC
Jasmin Blanchette
3
replies
[isabelle] Are there more general version of lfp/gfp lemmas with "while" combinator?
started 2016-07-28 09:04:29 UTC
2016-07-28 10:24:11 UTC
Alexander Kogtenkov via Cl-isabelle-users
2
replies
[isabelle] Operator clash for $
started 2016-06-16 09:57:07 UTC
2016-07-25 15:37:37 UTC
Makarius
1
reply
[isabelle] Private/qualified in locales
started 2016-07-07 15:20:17 UTC
2016-07-25 13:25:36 UTC
Makarius
2
replies
[isabelle] Eisbach match drule
started 2016-07-22 09:27:28 UTC
2016-07-25 10:52:40 UTC
M***@data61.csiro.au
2
replies
[isabelle] Printing full ML output in Isabelle/jEdit
started 2016-07-24 09:40:53 UTC
2016-07-24 09:56:00 UTC
Lars Hupel
3
replies
[isabelle] No type arity itself
started 2016-07-23 14:02:53 UTC
2016-07-23 18:10:16 UTC
Manuel Eberl
2
replies
[isabelle] nonnegative quadratic polynomial
started 2016-07-19 14:15:18 UTC
2016-07-19 16:30:59 UTC
Omar Jasim
1
reply
[isabelle] a proof on primitive recursion
started 2016-07-18 12:13:24 UTC
2016-07-18 13:03:22 UTC
Alfio Martini
3
replies
[isabelle] simp only:
started 2016-07-14 12:05:40 UTC
2016-07-15 07:42:40 UTC
Andreas Lochbihler
6
replies
[isabelle] Clone detection for Isabelle theories
started 2016-07-13 14:22:47 UTC
2016-07-14 15:56:27 UTC
Lars Hupel
5
replies
[isabelle] automatically grade Isabelle homework?
started 2016-07-09 09:04:16 UTC
2016-07-14 13:57:18 UTC
Johannes Waldmann
4
replies
[isabelle] A tautological error?
started 2016-07-11 12:40:09 UTC
2016-07-14 09:35:42 UTC
Ken Kubota
Click to Load More...
Loading...