Newsgroup:
fa.isabelle
Add New Display Options
3
replies
[isabelle] pairs and friends
started 2016-09-29 11:18:14 UTC
2016-09-30 13:28:30 UTC
Dmitriy Traytel
3
replies
[isabelle] Problems with Code-Generator
started 2016-09-29 11:18:10 UTC
2016-09-30 13:28:28 UTC
Andreas Lochbihler
3
replies
[isabelle] Function definition
started 2016-09-27 08:11:43 UTC
2016-09-27 11:52:30 UTC
T***@data61.csiro.au
2
replies
[isabelle] Mutual coinduction
started 2016-09-19 17:15:55 UTC
2016-09-26 13:43:29 UTC
Thomas Sternagel
3
replies
[isabelle] Tactic failed for Friends
started 2016-09-26 11:21:27 UTC
2016-09-26 13:06:29 UTC
Manuel Eberl
1
reply
[isabelle] Mysterious behavior of "let"
started 2016-09-19 17:15:51 UTC
2016-09-19 17:15:53 UTC
Andreas Lochbihler
4
replies
[isabelle] Structuring a Modular Project
started 2016-09-19 17:15:41 UTC
2016-09-19 17:15:49 UTC
scott constable
4
replies
[isabelle] case rule and OF
started 2016-09-19 17:15:31 UTC
2016-09-19 17:15:39 UTC
Andreas Lochbihler
12
replies
[isabelle] AFP Incompleteness Entry
started 2016-09-16 22:30:00 UTC
2016-09-19 17:15:27 UTC
G***@data61.csiro.au
2
replies
[isabelle] Question about numerals
started 2016-08-13 15:38:30 UTC
2016-09-15 20:07:52 UTC
Lars Hupel
2
replies
[isabelle] Reconciling FinFuns in Distro and AFP
started 2016-09-01 13:57:15 UTC
2016-09-15 20:07:50 UTC
Lars Hupel
3
replies
[isabelle] Proof failed for datatype
started 2016-09-14 21:58:46 UTC
2016-09-15 20:07:48 UTC
C***@data61.csiro.au
1
reply
[isabelle] Behavior of configuration options in local theories
started 2016-09-01 13:57:17 UTC
2016-09-14 21:58:44 UTC
Makarius
1
reply
[isabelle] a question of formalization of parameterized-word (bit-vector)
started 2016-09-01 13:57:25 UTC
2016-09-01 13:57:27 UTC
C. Diekmann
24
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-09-01 13:57:13 UTC
Ken Kubota
2
replies
[isabelle] Telling auto to use an eisbach method
started 2016-09-01 13:57:07 UTC
2016-09-01 13:57:11 UTC
Lawrence Paulson
6
replies
[isabelle] sledgehammer issue
started 2016-08-31 15:11:31 UTC
2016-09-01 13:57:03 UTC
Jasmin Blanchette
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] 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
Click to Load More...
Loading...