Newsgroup:
fa.isabelle
Add New Display Options
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
2
replies
[isabelle] using oops in document preparation
started 2016-07-12 10:22:58 UTC
2016-07-12 10:52:05 UTC
Andreas Lochbihler
2
replies
[isabelle] using a remote server behind Isabelle/jEdit
started 2016-07-12 10:22:52 UTC
2016-07-12 10:44:22 UTC
Makarius
1
reply
[isabelle] "natural deduction" vs. Gentzen-style
started 2016-07-11 08:23:55 UTC
2016-07-11 09:30:36 UTC
Andreas Röhler
5
replies
[isabelle] Inequality assumption
started 2016-07-05 15:25:36 UTC
2016-07-08 10:23:17 UTC
Lawrence Paulson
1
reply
[isabelle] Isabelle and the text console
started 2016-07-08 09:59:32 UTC
2016-07-08 10:19:06 UTC
Lawrence Paulson
Click to Load More...
Loading...