Newsgroup:
fa.isabelle
Add New Display Options
5
replies
[isabelle] New in the AFP: Intersecting Chords Theorem
started 2016-10-11 10:32:22 UTC
2016-10-13 16:55:38 UTC
Lawrence Paulson
5
replies
[isabelle] finishing a proof
started 2016-10-11 16:07:07 UTC
2016-10-13 16:55:34 UTC
Alexander Kogtenkov via Cl-isabelle-users
4
replies
[isabelle] Isabelle2016-1-RC0 available for testing
started 2016-10-06 10:10:52 UTC
2016-10-13 13:20:59 UTC
Lars Hupel
5
replies
[isabelle] Using an assumption as a rule
started 2016-10-06 09:31:47 UTC
2016-10-06 10:10:50 UTC
Peter Lammich
2
replies
[isabelle] Help defining a mutually recursive function
started 2016-10-05 09:57:40 UTC
2016-10-06 09:31:45 UTC
Corey Richardson
1
reply
[isabelle] Model checking of Simulink components with Isabelle
started 2016-10-01 14:20:53 UTC
2016-10-04 09:44:00 UTC
Viorel Preoteasa
4
replies
[isabelle] pairs and friends
started 2016-09-29 11:18:14 UTC
2016-10-01 14:20:55 UTC
Thomas Sternagel
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
Click to Load More...
Loading...